proposition: 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: 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. destruct 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). split with 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. Defined.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders