proposition: Lemma iseqrelabgrdiff (X : abmonoid) : iseqrel (hrelabgrdiff X).
proof: 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). Defined.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids