Lemma isbinophrelabgrdiff (X : abmonoid) : @isbinophrel (abmonoiddirprod X X) (hrelabgrdiff X). Proof. apply (@isbinophrellogeqf (abmonoiddirprod X X) _ _ (logeqhrelsabgrdiff X)). split. intros a b c r. apply (pr1 (isbinophrelabmonoidfrac X (totalsubmonoid X)) _ _ (pr1 c ,, make_carrier (λ x : X, htrue) (pr2 c) tt) r). intros a b c r. apply (pr2 (isbinophrelabmonoidfrac X (totalsubmonoid X)) _ _ (pr1 c ,, make_carrier (λ x : X, htrue) (pr2 c) tt) r). Qed.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.