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