proposition: Lemma module_mult_assoc {R : ring} {M : module R} (r s : R) (x : M) : (op2 r s) * x = r * (s * x).
proof: Proof. exact (maponpaths (λ r, pr1setofendabgr r x) (pr1 (pr2 (pr2 (pr2module M))) r s)). Defined.
imports: UniMath.MoreFoundations.Tactics UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.Monoids