Lemma iscomprelabmonoidfracrelint (X : abmonoid) (A : subabmonoid X) {L : hrel X} (is : ispartbinophrel A L) : iscomprelrel (eqrelabmonoidfrac X A) (abmonoidfracrelint X A L). Proof. set (assoc := (assocax X) : isassoc (@op X)). unfold isassoc in assoc. set (comm := commax X). unfold iscomm in comm. set (rer := abmonoidrer X). apply iscomprelrelif. apply (eqrelsymm (eqrelabmonoidfrac X A)). - intros xa xa' yb. unfold hrelabmonoidfrac. simpl. apply (@hinhfun2). intros t2e t2l. induction t2e as [ c1a e ]. induction t2l as [ c0a l ]. set (x := pr1 xa). set (a := pr1 (pr2 xa)). set (x' := pr1 xa'). set (a' := pr1 (pr2 xa')). set (y := pr1 yb). set (b := pr1 (pr2 yb)). set (c0 := pr1 c0a). set (c1 := pr1 c1a). exists ((pr2 xa) + c1a + c0a). change (L ((x' + b) + ((a + c1) + c0)) ((y + a') + ((a + c1) + c0))). change (x + a' + c1 = x' + a + c1) in e. rewrite (rer x' _ _ c0). induction (assoc x' a c1). induction e. rewrite (assoc x a' c1). rewrite (rer x _ _ c0). rewrite (assoc a c1 c0). rewrite (rer _ a' a _). rewrite (assoc a' c1 c0). rewrite (comm a' _). rewrite (comm c1 _). rewrite (assoc c0 c1 a'). induction (assoc (x + b) c0 (@op X c1 a')). induction (assoc (y + a) c0 (@op X c1 a')). apply ((pr2 is) _ _ _ (pr2 (@op A c1a (pr2 xa'))) l). - intros xa yb yb'. unfold hrelabmonoidfrac. simpl. apply (@hinhfun2). intros t2e t2l. induction t2e as [ c1a e ]. induction t2l as [ c0a l ]. set (x := pr1 xa). set (a := pr1 (pr2 xa)). set (y' := pr1 yb'). set (b' := pr1 (pr2 yb')). set (y := pr1 yb). set (b := pr1 (pr2 yb)). set (c0 := pr1 c0a). set (c1 := pr1 c1a). exists ((pr2 yb) + c1a + c0a). change (L ((x + b') + ((b + c1) + c0)) ((y' + a) + ((b + c1) + c0))). change (y + b' + c1 = y' + b + c1) in e. rewrite (rer y' _ _ c0). induction (assoc y' b c1). induction e. rewrite (assoc y b' c1). rewrite (rer y _ _ c0). rewrite (assoc b c1 c0). rewrite (rer _ b' b _). rewrite (assoc b' c1 c0). rewrite (comm b' _). rewrite (comm c1 _). rewrite (assoc c0 c1 b'). induction (assoc (x + b) c0 (@op X c1 b')). induction (assoc (y + a) c0 (@op X c1 b')). apply ((pr2 is) _ _ _ (pr2 (@op A c1a (pr2 yb'))) l). Qed.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.