Definition hrel0abmonoidfrac (X : abmonoid) (A : submonoid X) : hrel (X × A) := λ xa yb : setdirprod X A, (pr1 xa + pr1 (pr2 yb) = pr1 yb + pr1 (pr2 xa))%logic.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.