proposition: Lemma isbinophrelabmonoidfrac (X : abmonoid) (A : submonoid X) : @isbinophrel (setwithbinopdirprod X A) (eqrelabmonoidfrac X A).
proof: Proof. intros. apply (isbinopreflrel (eqrelabmonoidfrac X A) (eqrelrefl (eqrelabmonoidfrac X A))). set (rer := abmonoidoprer (pr2 X)). intros a b c d. simpl. apply hinhfun2. destruct a as [ a a' ]. destruct a' as [ a' isa' ]. destruct b as [ b b' ]. destruct b' as [ b' isb' ]. destruct c as [ c c' ]. destruct c' as [ c' isc' ]. destruct d as [ d d' ]. destruct d' as [ d' isd' ]. intros ax ay. destruct ax as [ a1 eq1 ]. destruct ay as [ a2 eq2 ]. split with (@op A a1 a2). destruct a1 as [ a1 aa1 ]. destruct 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). destruct eq1. destruct eq2. apply idpath. Defined.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders