(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


Set Automatic Coercions Import.
Set Implicit Arguments.
Unset Strict Implicit.
Require Export Ring_facts.
Require Export Generated_module.
Section ideals.
Variable R : RING.

Definition is_ideal (I : subgroup R) :=
  forall x : R, in_part x I -> forall a : R, in_part (ring_mult a x) I.

Record ideal : Type := 
  {ideal_subgroup :> subgroup R; ideal_prf : is_ideal ideal_subgroup}.

Lemma ideal_prop :
 forall (I : ideal) (x : I) (a : R), in_part (ring_mult a (I x)) I.
(* Goal: forall (I : ideal) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (@group_of_subgroup (abelian_group_group (ring_group R)) (ideal_subgroup I)))))) (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R a (@subtype_image_inj (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (ideal_subgroup I))))) x)) (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (ideal_subgroup I)))) *)
intros I x a; try assumption.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R a (@subtype_image_inj (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (ideal_subgroup I))))) x)) (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (ideal_subgroup I)))) *)
apply (ideal_prf (i:=I)).
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@subtype_image_inj (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (ideal_subgroup I))))) x) (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (ideal_subgroup I)))) *)
case x; simpl in |- *; auto with algebra.
Qed.

Lemma ideal_prop2 :
 forall (I : ideal) (x a : R), in_part x I -> in_part (ring_mult a x) I.
(* Goal: forall (I : ideal) (x a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (ideal_subgroup I))))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R a x) (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (ideal_subgroup I)))) *)
intros I x a H'; try assumption.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R a x) (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (ideal_subgroup I)))) *)
apply (ideal_prf (i:=I)); auto with algebra.
Qed.

Lemma ideal_prop3 :
 forall (I : ideal) (x y : R),
 in_part x I -> in_part y I -> in_part (sgroup_law R x y) I.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x x *)
auto with algebra.
Qed.

Lemma ideal_prop4 :
 forall (I : ideal) (x : R), in_part x I -> in_part (group_inverse R x) I.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x x *)
auto with algebra.
Qed.
End ideals.
Hint Resolve ideal_prop2: algebra.
Section Ring_as_module.
Variable R : ring.

Definition ring_module : module R.
apply
 (BUILD_MODULE_GROUP (R:=R) (module_util_G:=R)
    (gen_module_op:=fun a x : R => ring_mult a x));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x x *)
 abstract auto with algebra.
Defined.
End Ring_as_module.
Coercion ring_module : ring >-> module.
Section Generated_ideal.
Variable R : RING.
Variable A : part_set R.

Definition generated_module_subgroup : subgroup R.
apply (BUILD_SUB_GROUP (G:=R) (H:=generated_module (R:=R) (Mod:=R) A));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x x *)
 simpl in |- *; auto with algebra.
(* Goal: forall (x y : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x0 : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0)))) (_ : @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x0 : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) y (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0)))), @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x0 : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) x y) (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0))) *)
(* Goal: @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_on_def (group_monoid (abelian_group_group (ring_group R))))) (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x))) *)
(* Goal: forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x0 : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0)))), @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x0 : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (group_inverse (abelian_group_group (ring_group R)) x) (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0))) *)
intros x y H' H'0; try assumption.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
elim H'0; intros x0 E; elim E; intros H'1 H'2; try exact H'2; clear E H'0.
(* Goal: @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x0 : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) x y) (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0))) *)
(* Goal: @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_on_def (group_monoid (abelian_group_group (ring_group R))))) (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x))) *)
(* Goal: forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x0 : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0)))), @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x0 : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (group_inverse (abelian_group_group (ring_group R)) x) (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0))) *)
elim H'; intros x1 E; elim E; intros H'0 H'3; try exact H'3; clear E H'.
(* Goal: @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x0 : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) x y) (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0))) *)
(* Goal: @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_on_def (group_monoid (abelian_group_group (ring_group R))))) (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x))) *)
(* Goal: forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x0 : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0)))), @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x0 : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (group_inverse (abelian_group_group (ring_group R)) x) (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0))) *)
exists (Law x1 x0); split; [ try assumption | idtac ].
(* Goal: forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (Unit R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Inv R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (c : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Op R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) c f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
simpl in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) x y) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x1) (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0)) *)
(* Goal: @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_on_def (group_monoid (abelian_group_group (ring_group R))))) (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x))) *)
(* Goal: forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x0 : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0)))), @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x0 : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (group_inverse (abelian_group_group (ring_group R)) x) (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0))) *)
exact (SGROUP_comp (E:=R) H'3 H'2).
(* Goal: @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_on_def (group_monoid (abelian_group_group (ring_group R))))) (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x))) *)
(* Goal: forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x0 : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0)))), @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x0 : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (group_inverse (abelian_group_group (ring_group R)) x) (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0))) *)
exists (Unit R A); split; [ idtac | try assumption ].
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x x *)
auto with algebra.
(* Goal: forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (Unit R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Inv R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (c : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Op R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) c f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
simpl in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x x *)
auto with algebra.
(* Goal: forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x0 : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0)))), @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x0 : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (group_inverse (abelian_group_group (ring_group R)) x) (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0))) *)
intros x H'; try assumption.
(* Goal: @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x0 : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R a x) (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0))) *)
elim H'; intros x0 E; elim E; intros H'0 H'1; try exact H'1; clear E H'.
(* Goal: @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x0 : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (group_inverse (abelian_group_group (ring_group R)) x) (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0))) *)
exists (Inv x0); split; [ idtac | try assumption ].
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x x *)
auto with algebra.
(* Goal: forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (Unit R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Inv R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (c : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Op R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) c f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
simpl in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (group_inverse (abelian_group_group (ring_group R)) x) (group_inverse (abelian_group_group (ring_group R)) (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0)) *)
exact (GROUP_comp (G:=R) H'1).
Defined.

Definition generated_ideal : ideal R.
(* Goal: ideal R *)
apply (Build_ideal (R:=R) (ideal_subgroup:=generated_module_subgroup)).
(* Goal: @included (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R generated_ideal)))) *)
red in |- *.
(* Goal: forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (Unit R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Inv R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (c : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Op R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) c f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
simpl in |- *.
(* Goal: forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x0 : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0)))) (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))), @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x0 : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R a x) (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0))) *)
intros x H' a; try assumption.
(* Goal: @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x0 : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R a x) (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0))) *)
elim H'; intros x0 E; elim E; intros H'0 H'1; try exact H'1; clear E H'.
(* Goal: @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x0 : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R a x) (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0))) *)
exists (Op a x0); split; [ idtac | try assumption ].
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x x *)
auto with algebra.
(* Goal: forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (Unit R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Inv R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (c : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Op R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) c f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
simpl in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult R a x) (@module_mult R (ring_module R) a (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0)) *)
exact (MODULE_comp (R:=R) (Mod:=R:MODULE R) (Refl a) H'1).
Defined.

Lemma generated_ideal_included : included A generated_ideal.
(* Goal: @included (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R generated_ideal)))) *)
red in |- *.
(* Goal: forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (Unit R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Inv R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (c : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Op R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) c f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
simpl in |- *.
intros x H';
 exists (Var R (V:=A) (Build_subtype (E:=R) (P:=A) (subtype_elt:=x) H'));
 split; [ idtac | try assumption ].
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x x *)
auto with algebra.
(* Goal: forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (Unit R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Inv R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (c : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Op R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) c f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
simpl in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x x *)
auto with algebra.
Qed.

Lemma generated_ideal_minimal :
 forall I : ideal R, included A I -> included generated_ideal I.
(* Goal: forall (I : ideal R) (_ : @included (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))), @included (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R generated_ideal)))) (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
unfold included in |- *.
(* Goal: forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (Unit R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Inv R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (c : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Op R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) c f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
simpl in |- *.
(* Goal: forall (I : ideal R) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x A), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @ex (FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (fun x0 : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) => and True (@Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0)))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
intros I H' x H'0; try assumption.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
elim H'0; intros x0 E; elim E; intros H'1 H'2; try exact H'2; clear E H'0.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
generalize H'2; clear H'2; clear H'1.
(* Goal: forall _ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
generalize x; clear x.
(* Goal: forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) x0)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
elim x0.
(* Goal: forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (Unit R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Inv R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (c : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Op R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) c f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
simpl in |- *.
(* Goal: forall (c : @subtype (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subtype_elt (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A c)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (f0 : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f0)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Law R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) f f0))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (Unit R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Inv R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (c : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Op R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) c f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
intros c x H'0; try assumption.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (f0 : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f0)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Law R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) f f0))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (Unit R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Inv R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (c : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Op R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) c f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
apply H'.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x x *)
apply in_part_comp_l with (subtype_elt c); auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x x *)
case c; auto with algebra.
(* Goal: forall (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (f0 : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f0)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Law R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) f f0))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (Unit R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Inv R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (c : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Op R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) c f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
intros f H'0 f0 H'1 x H'2; try assumption.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (Unit R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Inv R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (c : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Op R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) c f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
simpl in H'2.
apply
 in_part_comp_l
  with
    (sgroup_law R
       (FMd_lift_fun (R:=R) (V:=A) (Mod:=R:MODULE R) (inj_part A) f)
       (FMd_lift_fun (R:=R) (V:=A) (Mod:=R:MODULE R) (inj_part A) f0));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x x *)
 auto with algebra.
(* Goal: forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (Unit R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Inv R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (c : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Op R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) c f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
simpl in |- *.
(* Goal: forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_on_def (group_monoid (abelian_group_group (ring_group R)))))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Inv R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (c : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Op R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) c f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
intros x H'0; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x x *)
apply in_part_comp_l with (monoid_unit R); auto with algebra.
(* Goal: forall (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Inv R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
(* Goal: forall (c : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Op R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) c f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
intros f H'0 x H'1; try assumption.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
simpl in H'1.
apply
 in_part_comp_l
  with
    (group_inverse R
       (FMd_lift_fun (R:=R) (V:=A) (Mod:=R:MODULE R) (inj_part A) f));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x x *)
 auto with algebra.
(* Goal: forall (c : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (f : FMd R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A))) (_ : forall (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) f)), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@FMd_lift_fun R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) (ring_module R) (@inj_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A) (@Op R (@set_of_subtype_image (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) A)) c f))), @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
intros c f H'0 x H'1; try assumption.
(* Goal: @in_part (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x (@subsgroup_part (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (@submonoid_subsgroup (group_monoid (abelian_group_group (ring_group R))) (@subgroup_submonoid (abelian_group_group (ring_group R)) (@ideal_subgroup R I)))) *)
simpl in H'1.
apply
 in_part_comp_l
  with
    (module_mult c
       (FMd_lift_fun (R:=R) (V:=A) (Mod:=R:MODULE R) (inj_part A) f));
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x x *)
 auto with algebra.
change
  (in_part
     (ring_mult c
        (FMd_lift_fun (R:=R) (V:=A) (Mod:=R:MODULE R) (inj_part A) f))
     (subsgroup_part
        (submonoid_subsgroup (subgroup_submonoid (ideal_subgroup I)))))
 in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) x x *)
apply ideal_prop2; auto with algebra.
Qed.
End Generated_ideal.
Hint Resolve generated_ideal_minimal generated_ideal_included: algebra.
