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