proposition: Lemma iscomprelabmonoidfracrelint (X : abmonoid) (A : subabmonoid X) {L : hrel X} (is : ispartbinophrel A L) : iscomprelrel (eqrelabmonoidfrac X A) (abmonoidfracrelint X A L).
proof: 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. destruct t2e as [ c1a e ]. destruct 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). split with ((pr2 xa) + c1a + c0a). change (L ((x' + b) + ((a + c1) + c0)) ((y + a') + ((a + c1) + c0))). change (paths (x + a' + c1) (x' + a + c1)) in e. rewrite (rer x' _ _ c0). destruct (assoc x' a c1). destruct 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'). destruct (assoc (x + b) c0 (@op X c1 a')). destruct (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. destruct t2e as [ c1a e ]. destruct 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). split with ((pr2 yb) + c1a + c0a). change (L ((x + b') + ((b + c1) + c0)) ((y' + a) + ((b + c1) + c0))). change (paths (y + b' + c1) (y' + b + c1)) in e. rewrite (rer y' _ _ c0). destruct (assoc y' b c1). destruct 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'). destruct (assoc (x + b) c0 (@op X c1 b')). destruct (assoc (y + a) c0 (@op X c1 b')). apply ((pr2 is) _ _ _ (pr2 (@op A c1a (pr2 yb'))) l). Defined.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders