Lemma istransabmonoidfracrelint (X : abmonoid) (A : subabmonoid X) {L : hrel X} (is : ispartbinophrel A L) (isl : istrans L) : istrans (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). intros xa1 xa2 xa3. unfold abmonoidfracrelint. simpl. apply hinhfun2. intros t2l1 t2l2. set (c1a := pr1 t2l1). set (l1 := pr2 t2l1). set (c2a := pr1 t2l2). set (l2 := pr2 t2l2). set (x1 := pr1 xa1). set (a1 := pr1 (pr2 xa1)). set (x2 := pr1 xa2). set (a2 := pr1 (pr2 xa2)). set (x3 := pr1 xa3). set (a3 := pr1 (pr2 xa3)). set (c1 := pr1 c1a). set (c2 := pr1 c2a). exists ((pr2 xa2) + (@op A c1a c2a)). change (L ((x1 + a3) + (a2 + (c1 + c2))) ((x3 + a1) + (a2 + (c1 + c2)))). assert (ll1 : L ((x1 + a3) + (a2 + (@op X c1 c2))) (((x2 + a1) + c1) + (c2 + a3))). { rewrite (rer _ a3 a2 _). rewrite (comm a3 (@op X c1 c2)). rewrite (assoc c1 c2 a3). induction (assoc (x1 + a2) c1 (@op X c2 a3)). apply ((pr2 is) _ _ _ (pr2 (@op A c2a (pr2 xa3))) l1). } assert (ll2 : L (((x2 + a3) + c2) + (@op X a1 c1)) ((x3 + a1) + (a2 + (@op X c1 c2)))). { rewrite (rer _ a1 a2 _). induction (assoc a1 c1 c2). rewrite (comm (a1 + c1) c2). induction (assoc (x3 + a2) c2 (@op X a1 c1)). apply ((pr2 is) _ _ _ (pr2 (@op A (pr2 xa1) c1a)) l2). } assert (e : x2 + a1 + c1 + (c2 + a3) = x2 + a3 + c2 + (a1 + c1)). { rewrite (assoc (x2 + a1) c1 _). rewrite (assoc (x2 + a3) c2 _). rewrite (assoc x2 a1 _). rewrite (assoc x2 a3 _). induction (assoc a1 c1 (c2 + a3)). induction (assoc a3 c2 (a1 + c1)). induction (comm (c2 + a3) (a1 + c1)). rewrite (comm a3 c2). apply idpath. } induction e. apply (isl _ _ _ ll1 ll2). Qed.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.