Definition hrelabgrdiff (X : abmonoid) : hrel (X × X) := λ xa1 xa2, ∃ (x0 : X), (pr1 xa1 + pr2 xa2) + x0 = (pr1 xa2 + pr2 xa1) + x0.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.