fact: Definition abgrdiffinvint (X : abmonoid) : dirprod X X -> dirprod X X := λ xs : _, make_dirprod (pr2 xs) (pr1 xs).
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids