fact: Definition abmonoid_of_monoid (X : monoid) (H : iscomm (@op X)) : abmonoid := make_abmonoid X (make_isabmonoidop (pr2 X) H).
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders