proposition: 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)).
proof: Proof. exact (module_op_lin_left_prf Mod). Qed.
imports: Module_cat Abelian_group_facts