proposition: Lemma MODULE_absorbant_l : forall x : Mod, Equal (module_mult (monoid_unit R) x) (monoid_unit Mod).
proof: Proof. intros x; try assumption. 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. apply Trans with (module_mult (monoid_unit R) x); auto with algebra. Qed.
imports: Module_cat Abelian_group_facts