proposition: Lemma MODULE_assoc : forall (a b : R) (x : Mod), Equal (module_mult (ring_mult a b) x) (module_mult a (module_mult b x)).
proof: Proof. exact (operation_assoc (module_op Mod)). Qed.
imports: Module_cat Abelian_group_facts