fact: Definition binopeqrelabmonoidfrac (X : abmonoid) (A : subabmonoid X) : binopeqrel (abmonoiddirprod X A) := @make_binopeqrel (setwithbinopdirprod X A) (eqrelabmonoidfrac X A) (isbinophrelabmonoidfrac X A).
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders