Lemma isbinophrelabmonoidfrac (X : abmonoid) (A : submonoid X) : @isbinophrel (setwithbinopdirprod X A) (eqrelabmonoidfrac X A). Proof. intros. apply (isbinopreflrel (eqrelabmonoidfrac X A) (eqrelrefl (eqrelabmonoidfrac X A))). set (rer := abmonoidoprer (pr2 X)). intros a b c d. simpl. apply hinhfun2. induction a as [ a a' ]. induction a' as [ a' isa' ]. induction b as [ b b' ]. induction b' as [ b' isb' ]. induction c as [ c c' ]. induction c' as [ c' isc' ]. induction d as [ d d' ]. induction d' as [ d' isd' ]. intros ax ay. induction ax as [ a1 eq1 ]. induction ay as [ a2 eq2 ]. exists (@op A a1 a2). induction a1 as [ a1 aa1 ]. induction a2 as [ a2 aa2 ]. simpl in *. rewrite (rer a c b' d'). rewrite (rer b d a' c'). rewrite (rer (a + b') (c + d') a1 a2). rewrite (rer (b + a') (d + c') a1 a2). induction eq1. induction eq2. apply idpath. Qed.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.