Lemma ispartlbinopabmonoidfracrel (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 ((prabmonoidfrac X A (pr1 aa) aa') + z) ((prabmonoidfrac X A (pr1 aa) aa') + z'). 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', isaprop (abmonoidfracrel X A is z z' → abmonoidfracrel X A is (prabmonoidfrac X A (pr1 aa) aa' + z) (prabmonoidfrac X A (pr1 aa) aa' + z'))). { 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) (pr1 aa ,, aa') xa1) (@op (abmonoiddirprod X A) (pr1 aa ,, aa') xa2)). 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 (a + x1 + (a' + a2) + c0) (a + x2 + (a' + a1) + c0)). rewrite (rer _ x1 a' _). rewrite (rer _ x2 a' _). rewrite (assoc _ (x1 + a2) c0). rewrite (assoc _ (x2 + a1) c0). apply ((pr1 is) _ _ _ (pr2 (@op A aa aa'))). apply l. Qed.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.