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