Definition abmonoidfracrelint (X : abmonoid) (A : subabmonoid X) (L : hrel X) : hrel (setwithbinopdirprod X A) := λ xa yb, ∃ (c0 : A), L (((pr1 xa) + (pr1 (pr2 yb))) + (pr1 c0)) (((pr1 yb) + (pr1 (pr2 xa))) + (pr1 c0)).
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.