Lemma ispartrbinopabmonoidfracrel (X : abmonoid) (A : subabmonoid X) {L : hrel X} (is : ispartbinophrel A L) (aa aa' : A) (z z' : abmonoidfrac X A) (l : abmonoidfracrel X A is z z') : abmonoidfracrel X A is (z + (prabmonoidfrac X A (pr1 aa) aa')) (z' + (prabmonoidfrac X A (pr1 aa) aa')). Proof. revert z z' l. set (assoc := (assocax X) : isassoc (@op X)). unfold isassoc in assoc. set (comm := commax X). unfold iscomm in comm. set (rer := abmonoidrer X). assert (int : ∏ (z z' : abmonoidfrac X A), isaprop (abmonoidfracrel X A is z z' → abmonoidfracrel X A is (z + (prabmonoidfrac X A (pr1 aa) aa')) (z' + prabmonoidfrac X A (pr1 aa) aa'))). { intros z z'. apply impred. intro. apply (pr2 (abmonoidfracrel _ _ _ _ _)). } apply (setquotuniv2prop _ (λ z z', make_hProp _ (int z z'))). intros xa1 xa2. change (abmonoidfracrelint X A L xa1 xa2 → abmonoidfracrelint X A L (@op (abmonoiddirprod X A) xa1 (pr1 aa ,, aa')) (@op (abmonoiddirprod X A) xa2 (pr1 aa ,, aa'))). unfold abmonoidfracrelint. simpl. apply hinhfun. intro t2l. set (a := pr1 aa). set (a' := pr1 aa'). set (c0a := pr1 t2l). set (l := pr2 t2l). set (c0 := pr1 c0a). set (x1 := pr1 xa1). set (a1 := pr1 (pr2 xa1)). set (x2 := pr1 xa2). set (a2 := pr1 (pr2 xa2)). exists c0a. change (L (x1 + a + (a2 + a') + c0) (x2 + a + (a1 + a') + c0)). rewrite (rer _ a a2 _). rewrite (rer _ a a1 _). rewrite (assoc (x1 + a2) _ c0). rewrite (assoc (x2 + a1) _ c0). rewrite (comm _ c0). induction (assoc (x1 + a2) c0 (a + a')). induction (assoc (x2 + a1) c0 (a + a')). apply ((pr2 is) _ _ _ (pr2 (@op A aa aa'))). apply l. Qed.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.