Definition binopeqrelabmonoidfrac (X : abmonoid) (A : subabmonoid X) : binopeqrel (abmonoiddirprod X A) := @make_binopeqrel (setwithbinopdirprod X A) (eqrelabmonoidfrac X A) (isbinophrelabmonoidfrac X A).
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.