Lemma iseqrelabgrdiff (X : abmonoid) : iseqrel (hrelabgrdiff X). Proof. apply (iseqrellogeqf (logeqhrelsabgrdiff X)). apply (iseqrelconstr). intros xx' xx'' xx'''. intros r1 r2. apply (eqreltrans (eqrelabmonoidfrac X (totalsubmonoid X)) _ _ _ r1 r2). intro xx. apply (eqrelrefl (eqrelabmonoidfrac X (totalsubmonoid X)) _). intros xx xx'. intro r. apply (eqrelsymm (eqrelabmonoidfrac X (totalsubmonoid X)) _ _ r). Qed.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.