proposition: Lemma MODULE_dist_l : forall (a : R) (x y : Mod), Equal (module_mult a (sgroup_law Mod x y)) (sgroup_law Mod (module_mult a x) (module_mult a y)).
proof: Proof. exact (module_op_lin_right_prf Mod). Qed.
imports: Module_cat Abelian_group_facts