proposition: Lemma holds_monoid_mul_assoc : holds (monoid_algebra M) monoid_mul_assoc.
proof: Proof. intro. change (op (op (α 0) (α 1)) (α 2) = op (α 0) (op (α 1) (α 2))). apply assocax. Qed.
imports: UniMath.MoreFoundations.Notations UniMath.Combinatorics.StandardFiniteSets UniMath.Algebra.Monoids UniMath.Algebra.Universal.EqAlgebras