(* 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 Module_cat.
Require Export Abelian_group_facts.
Section Lemmas.
Variable R : RING.
Variable Mod : MODULE R.

Lemma MODULE_comp :
 forall (a b : R) (x y : Mod),
 Equal a b -> Equal x y -> Equal (module_mult a x) (module_mult b y).
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x y : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))))) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) a b) (_ : @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) x y), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@module_mult R Mod a x) (@module_mult R Mod b y) *)
intros a b x y H' H'0; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@module_mult R Mod a x) (@module_mult R Mod b y) *)
apply Trans with (module_mult a y); unfold module_mult in |- *.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@Ap (sgroup_set (monoid_sgroup (@Build_monoid (monoid_sgroup (@Build_monoid (@Build_sgroup (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult_sgroup (ring_group R) (ring_on_def R))) (@ring_mult_monoid (ring_group R) (ring_on_def R)))) (@ring_monoid (ring_group R) (ring_on_def R))))) (sgroup_set (monoid_sgroup (Endo_SET (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))))))) (@sgroup_map (monoid_sgroup (@Build_monoid (monoid_sgroup (@Build_monoid (@Build_sgroup (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult_sgroup (ring_group R) (ring_on_def R))) (@ring_mult_monoid (ring_group R) (ring_on_def R)))) (@ring_monoid (ring_group R) (ring_on_def R)))) (monoid_sgroup (Endo_SET (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))))) (@monoid_sgroup_hom (@Build_monoid (monoid_sgroup (@Build_monoid (@Build_sgroup (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult_sgroup (ring_group R) (ring_on_def R))) (@ring_mult_monoid (ring_group R) (ring_on_def R)))) (@ring_monoid (ring_group R) (ring_on_def R))) (Endo_SET (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))))) (@module_op R (@module_carrier R Mod) (@module_on_def R Mod)))) a) y) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@Ap (sgroup_set (monoid_sgroup (@Build_monoid (monoid_sgroup (@Build_monoid (@Build_sgroup (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult_sgroup (ring_group R) (ring_on_def R))) (@ring_mult_monoid (ring_group R) (ring_on_def R)))) (@ring_monoid (ring_group R) (ring_on_def R))))) (sgroup_set (monoid_sgroup (Endo_SET (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))))))) (@sgroup_map (monoid_sgroup (@Build_monoid (monoid_sgroup (@Build_monoid (@Build_sgroup (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult_sgroup (ring_group R) (ring_on_def R))) (@ring_mult_monoid (ring_group R) (ring_on_def R)))) (@ring_monoid (ring_group R) (ring_on_def R)))) (monoid_sgroup (Endo_SET (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))))) (@monoid_sgroup_hom (@Build_monoid (monoid_sgroup (@Build_monoid (@Build_sgroup (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult_sgroup (ring_group R) (ring_on_def R))) (@ring_mult_monoid (ring_group R) (ring_on_def R)))) (@ring_monoid (ring_group R) (ring_on_def R))) (Endo_SET (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))))) (@module_op R (@module_carrier R Mod) (@module_on_def R Mod)))) b) y) *)
apply Ap_comp; auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@Ap (sgroup_set (monoid_sgroup (@Build_monoid (monoid_sgroup (@Build_monoid (@Build_sgroup (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult_sgroup (ring_group R) (ring_on_def R))) (@ring_mult_monoid (ring_group R) (ring_on_def R)))) (@ring_monoid (ring_group R) (ring_on_def R))))) (sgroup_set (monoid_sgroup (Endo_SET (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))))))) (@sgroup_map (monoid_sgroup (@Build_monoid (monoid_sgroup (@Build_monoid (@Build_sgroup (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult_sgroup (ring_group R) (ring_on_def R))) (@ring_mult_monoid (ring_group R) (ring_on_def R)))) (@ring_monoid (ring_group R) (ring_on_def R)))) (monoid_sgroup (Endo_SET (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))))) (@monoid_sgroup_hom (@Build_monoid (monoid_sgroup (@Build_monoid (@Build_sgroup (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult_sgroup (ring_group R) (ring_on_def R))) (@ring_mult_monoid (ring_group R) (ring_on_def R)))) (@ring_monoid (ring_group R) (ring_on_def R))) (Endo_SET (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))))) (@module_op R (@module_carrier R Mod) (@module_on_def R Mod)))) a) y) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@Ap (sgroup_set (monoid_sgroup (@Build_monoid (monoid_sgroup (@Build_monoid (@Build_sgroup (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult_sgroup (ring_group R) (ring_on_def R))) (@ring_mult_monoid (ring_group R) (ring_on_def R)))) (@ring_monoid (ring_group R) (ring_on_def R))))) (sgroup_set (monoid_sgroup (Endo_SET (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))))))) (@sgroup_map (monoid_sgroup (@Build_monoid (monoid_sgroup (@Build_monoid (@Build_sgroup (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult_sgroup (ring_group R) (ring_on_def R))) (@ring_mult_monoid (ring_group R) (ring_on_def R)))) (@ring_monoid (ring_group R) (ring_on_def R)))) (monoid_sgroup (Endo_SET (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))))) (@monoid_sgroup_hom (@Build_monoid (monoid_sgroup (@Build_monoid (@Build_sgroup (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))) (@ring_mult_sgroup (ring_group R) (ring_on_def R))) (@ring_mult_monoid (ring_group R) (ring_on_def R)))) (@ring_monoid (ring_group R) (ring_on_def R))) (Endo_SET (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))))) (@module_op R (@module_carrier R Mod) (@module_on_def R Mod)))) b) y) *)
apply Ap_comp; auto with algebra.
Qed.

Lemma MODULE_assoc :
 forall (a b : R) (x : Mod),
 Equal (module_mult (ring_mult a b) x) (module_mult a (module_mult b x)).
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@module_mult R Mod (@ring_mult R a b) x) (@module_mult R Mod a (@module_mult R Mod b x)) *)
exact (operation_assoc (module_op Mod)).
Qed.

Lemma MODULE_dist_r :
 forall (a b : R) (x : Mod),
 Equal (module_mult (sgroup_law R a b) x)
   (sgroup_law Mod (module_mult a x) (module_mult b x)).
(* Goal: forall (a b : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@module_mult R Mod (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) a b) x) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (@module_mult R Mod a x) (@module_mult R Mod b x)) *)
exact (module_op_lin_left_prf Mod).
Qed.

Lemma MODULE_dist_l :
 forall (a : R) (x y : Mod),
 Equal (module_mult a (sgroup_law Mod x y))
   (sgroup_law Mod (module_mult a x) (module_mult a y)).
(* Goal: forall (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x y : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@module_mult R Mod a (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) x y)) (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (@module_mult R Mod a x) (@module_mult R Mod a y)) *)
exact (module_op_lin_right_prf Mod).
Qed.

Lemma MODULE_unit_l : forall x : Mod, Equal (module_mult (ring_unit R) x) x.
(* Goal: forall x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@module_mult R Mod (ring_unit R) x) x *)
exact (operation_unit (module_op Mod)).
Qed.
Hint Resolve MODULE_comp MODULE_dist_r MODULE_dist_l MODULE_assoc
  MODULE_unit_l: algebra.

Lemma MODULE_absorbant_l :
 forall x : Mod, Equal (module_mult (monoid_unit R) x) (monoid_unit Mod).
(* Goal: forall x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@module_mult R Mod (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_on_def (group_monoid (abelian_group_group (ring_group R))))) x) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (monoid_on_def (group_monoid (abelian_group_group (@module_carrier R Mod))))) *)
intros x; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@module_mult R Mod (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_on_def (group_monoid (abelian_group_group (ring_group R))))) x) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (monoid_on_def (group_monoid (abelian_group_group (@module_carrier R Mod))))) *)
apply GROUP_reg_left with (module_mult (monoid_unit R) x); auto with algebra.
apply
 Trans with (module_mult (sgroup_law R (monoid_unit R) (monoid_unit R)) x);
 auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@module_mult R Mod (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) a (group_inverse (abelian_group_group (ring_group R)) a)) x) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (monoid_on_def (group_monoid (abelian_group_group (@module_carrier R Mod))))) *)
apply Trans with (module_mult (monoid_unit R) x); auto with algebra.
Qed.

Lemma MODULE_absorbant_r :
 forall a : R, Equal (module_mult a (monoid_unit Mod)) (monoid_unit Mod).
(* Goal: forall a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@module_mult R Mod a (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (monoid_on_def (group_monoid (abelian_group_group (@module_carrier R Mod)))))) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (monoid_on_def (group_monoid (abelian_group_group (@module_carrier R Mod))))) *)
intros a; try assumption.
apply GROUP_reg_left with (module_mult a (monoid_unit (module_carrier Mod)));
 auto with algebra.
apply
 Trans
  with (module_mult a (sgroup_law Mod (monoid_unit Mod) (monoid_unit Mod)));
 auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@module_mult R Mod a (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) x (group_inverse (abelian_group_group (@module_carrier R Mod)) x))) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (monoid_on_def (group_monoid (abelian_group_group (@module_carrier R Mod))))) *)
apply Trans with (module_mult a (monoid_unit Mod)); auto with algebra.
Qed.

Lemma MODULE_mult_op_r :
 forall (a : R) (x : Mod),
 Equal (module_mult a (group_inverse Mod x))
   (group_inverse Mod (module_mult a x)).
(* Goal: forall (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@module_mult R Mod (group_inverse (abelian_group_group (ring_group R)) a) x) (group_inverse (abelian_group_group (@module_carrier R Mod)) (@module_mult R Mod a x)) *)
intros a x; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@module_mult R Mod (group_inverse (abelian_group_group (ring_group R)) a) x) (group_inverse (abelian_group_group (@module_carrier R Mod)) (@module_mult R Mod a x)) *)
apply Sym.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (group_inverse (abelian_group_group (@module_carrier R Mod)) (@module_mult R Mod a x)) (@module_mult R Mod (group_inverse (abelian_group_group (ring_group R)) a) x) *)
apply GROUP_law_inverse.
apply Trans with (module_mult a (sgroup_law Mod x (group_inverse Mod x)));
 auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@module_mult R Mod a (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) x (group_inverse (abelian_group_group (@module_carrier R Mod)) x))) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (monoid_on_def (group_monoid (abelian_group_group (@module_carrier R Mod))))) *)
apply Trans with (module_mult a (monoid_unit Mod)); auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@module_mult R Mod a (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (monoid_on_def (group_monoid (abelian_group_group (@module_carrier R Mod)))))) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (monoid_on_def (group_monoid (abelian_group_group (@module_carrier R Mod))))) *)
apply MODULE_absorbant_r.
Qed.

Lemma MODULE_mult_op_l :
 forall (a : R) (x : Mod),
 Equal (module_mult (group_inverse R a) x)
   (group_inverse Mod (module_mult a x)).
(* Goal: forall (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@module_mult R Mod (group_inverse (abelian_group_group (ring_group R)) a) x) (group_inverse (abelian_group_group (@module_carrier R Mod)) (@module_mult R Mod a x)) *)
intros a x; try assumption.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@module_mult R Mod (group_inverse (abelian_group_group (ring_group R)) a) x) (group_inverse (abelian_group_group (@module_carrier R Mod)) (@module_mult R Mod a x)) *)
apply Sym.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (group_inverse (abelian_group_group (@module_carrier R Mod)) (@module_mult R Mod a x)) (@module_mult R Mod (group_inverse (abelian_group_group (ring_group R)) a) x) *)
apply GROUP_law_inverse.
apply Trans with (module_mult (sgroup_law R a (group_inverse R a)) x);
 auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@module_mult R Mod (sgroup_law (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) a (group_inverse (abelian_group_group (ring_group R)) a)) x) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (monoid_on_def (group_monoid (abelian_group_group (@module_carrier R Mod))))) *)
apply Trans with (module_mult (monoid_unit R) x); auto with algebra.
(* Goal: @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (@module_mult R Mod (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))) (monoid_on_def (group_monoid (abelian_group_group (ring_group R))))) x) (@monoid_unit (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (monoid_on_def (group_monoid (abelian_group_group (@module_carrier R Mod))))) *)
apply MODULE_absorbant_l.
Qed.
Variable Mod' : MODULE R.
Variable f : Hom Mod Mod'.

Lemma MODULE_hom_prop :
 forall (a : R) (x : Mod), Equal (f (module_mult a x)) (module_mult a (f x)).
(* Goal: forall (a : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (ring_group R)))))) (x : Carrier (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))))), @Equal (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod'))))) (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod'))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod')))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (@module_carrier R Mod))) (group_monoid (abelian_group_group (@module_carrier R Mod'))) (@module_monoid_hom R Mod Mod' f))) (@module_mult R Mod a x)) (@module_mult R Mod' a (@Ap (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod))))) (sgroup_set (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod'))))) (@sgroup_map (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod)))) (monoid_sgroup (group_monoid (abelian_group_group (@module_carrier R Mod')))) (@monoid_sgroup_hom (group_monoid (abelian_group_group (@module_carrier R Mod))) (group_monoid (abelian_group_group (@module_carrier R Mod'))) (@module_monoid_hom R Mod Mod' f))) x)) *)
case f; auto with algebra.
Qed.
End Lemmas.
Hint Resolve MODULE_comp MODULE_assoc MODULE_dist_r MODULE_dist_l
  MODULE_unit_l MODULE_absorbant_l MODULE_absorbant_r MODULE_mult_op_l
  MODULE_mult_op_r MODULE_hom_prop: algebra.
