Lemma ispartbinopabmonoidfracrelint (X : abmonoid) (A : subabmonoid X) {L : hrel X} (is : ispartbinophrel A L) : @ispartbinophrel (setwithbinopdirprod X A) (λ xa, A (pr1 xa)) (abmonoidfracrelint X A L). Proof. intros. set (assoc := (assocax X) : isassoc (@op X)). unfold isassoc in assoc. set (comm := commax X). unfold iscomm in comm. set (rer := abmonoidrer X). apply ispartbinophrelif. apply (commax (abmonoiddirprod X A)). intros xa yb zc s. unfold abmonoidfracrelint. simpl. apply (@hinhfun). intro t2l. induction t2l as [ c0a l ]. set (x := pr1 xa). set (a := pr1 (pr2 xa)). set (y := pr1 yb). set (b := pr1 (pr2 yb)). set (z := pr1 zc). set (c := pr1 (pr2 zc)). set (c0 := pr1 c0a). exists c0a. change (L (((z + x) + (c + b)) + c0) (((z + y) + (c + a)) + c0)). change (pr1 (L ((x + b) + c0) ((y + a) + c0))) in l. rewrite (rer z _ _ b). rewrite (assoc (z + c) _ _). rewrite (rer z _ _ a). rewrite (assoc (z + c) _ _). apply ((pr1 is) _ _ _ (pr2 (@op A (make_carrier A z s) (pr2 zc)))). apply l. Qed.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.