fact: Definition abgr_of_gr (X : gr) (H : iscomm (@op X)) : abgr := make_abgr X (make_isabgrop (pr2 X) H).
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids