Lemma logeqhrelsabgrdiff (X : abmonoid) : hrellogeq (hrelabgrdiff' X) (hrelabgrdiff X). Proof. split. simpl. apply hinhfun. intro t2. set (a0 := pr1 (pr1 t2)). exists a0. apply (pr2 t2). simpl. apply hinhfun. intro t2. set (x0 := pr1 t2). exists (x0 ,, tt). apply (pr2 t2). Defined.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.