proposition: 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)).
proof: Proof. intros a x; try assumption. apply Sym. apply GROUP_law_inverse. apply Trans with (module_mult (sgroup_law R a (group_inverse R a)) x); auto with algebra. apply Trans with (module_mult (monoid_unit R) x); auto with algebra. apply MODULE_absorbant_l. Qed.
imports: Module_cat Abelian_group_facts