fact: Definition monoid_mul_assoc := mul (mul x y) z == mul x (mul y z).
imports: UniMath.MoreFoundations.Notations UniMath.Combinatorics.StandardFiniteSets UniMath.Algebra.Monoids UniMath.Algebra.Universal.EqAlgebras