proposition: Lemma isbinophrelabgrdiff (X : abmonoid) : @isbinophrel (abmonoiddirprod X X) (hrelabgrdiff X).
proof: Proof. apply (@isbinophrellogeqf (abmonoiddirprod X X) _ _ (logeqhrelsabgrdiff X)). split. intros a b c r. apply (pr1 (isbinophrelabmonoidfrac X (totalsubmonoid X)) _ _ (make_dirprod (pr1 c) (make_carrier (λ x : X, htrue) (pr2 c) tt)) r). intros a b c r. apply (pr2 (isbinophrelabmonoidfrac X (totalsubmonoid X)) _ _ (make_dirprod (pr1 c) (make_carrier (λ x : X, htrue) (pr2 c) tt)) r). Defined.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids