Lemma iscotransabmonoidfracrelint (X : abmonoid) (A : subabmonoid X) {L : hrel X} (is : ispartbinophrel A L) (isl : iscotrans L) : iscotrans (abmonoidfracrelint X A L). Proof. intros. set (assoc := (assocax X) : isassoc (@op X)). unfold isassoc in assoc. set (comm := (commax X) : iscomm (@op X)). unfold iscomm in comm. set (rer := abmonoidrer X). unfold iscotrans. intros xa1 xa2 xa3. unfold abmonoidfracrelint. simpl. apply (@hinhuniv _ (ishinh _)). intro t2. set (c0a := pr1 t2). set (l0 := pr2 t2). 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 (c0 := pr1 c0a). set (z1 := (x1 + a3 + (a2 + c0))). set (z2 := x2 + a1 + (a3 + c0)). set (z3 := x3 + a1 + (a2 + c0)). assert (int : L z1 z3). { unfold z1. unfold z3. rewrite (comm a2 c0). rewrite <- (assoc _ _ a2). rewrite <- (assoc _ _ a2). apply ((pr2 is) _ _ _ (pr2 (pr2 xa2)) l0). } set (int' := isl z1 z2 z3 int). generalize int'. clear int'. simpl. apply hinhfun. intro cc. induction cc as [ l12 | l23 ]. - apply ii1. apply hinhpr. exists ((pr2 xa3) + c0a). change (L (x1 + a2 + (a3 + c0)) (x2 + a1 + (a3 + c0))). rewrite (rer _ a2 a3 _). apply l12. - apply ii2. apply hinhpr. exists ((pr2 xa1) + c0a). change (L (x2 + a3 + (a1 + c0)) (x3 + a2 + (a1 + c0))). rewrite (rer _ a3 a1 _). rewrite (rer _ a2 a1 _). apply l23. Qed.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.