Lemma iseqrelabmonoidfrac (X : abmonoid) (A : submonoid X) : iseqrel (hrelabmonoidfrac X A). Proof. intros. set (assoc := assocax X). set (comm := commax X). set (R := hrelabmonoidfrac X A). apply iseqrelconstr. - unfold istrans. intros ab cd ef. simpl. apply hinhfun2. induction ab as [ a b ]. induction cd as [ c d ]. induction ef as [ e f ]. induction b as [ b isb ]. induction d as [ d isd ]. induction f as [ f isf ]. intros eq1 eq2. induction eq1 as [ x1 eq1 ]. induction eq2 as [ x2 eq2 ]. simpl in *. exists (@op A (d ,, isd) (@op A x1 x2)). induction x1 as [ x1 isx1 ]. induction x2 as [ x2 isx2 ]. induction A as [ A ax ]. simpl in *. rewrite (assoc a f (d + (x1 + x2))). rewrite (comm f (d + (x1 + x2))). induction (assoc a (d + (x1 + x2)) f). induction (assoc a d (x1 + x2)). induction (assoc (a + d) x1 x2). rewrite eq1. rewrite (comm x1 x2). rewrite (assoc e b (d + (x2 + x1))). rewrite (comm b (d + (x2 + x1))). induction (assoc e (d + (x2 + x1)) b). induction (assoc e d (x2 + x1)). induction (assoc (e + d) x2 x1). induction eq2. rewrite (assoc (c + b) x1 x2). rewrite (assoc (c + f) x2 x1). rewrite (comm x1 x2). rewrite (assoc (c + b) (x2 + x1) f). rewrite (assoc (c + f) (x2 + x1) b). rewrite (comm (x2 + x1) f). rewrite (comm (x2 + x1) b). induction (assoc (c + b) f (x2 + x1)). induction (assoc (c + f) b (x2 + x1)). rewrite (assoc c b f). rewrite (assoc c f b). rewrite (comm b f). apply idpath. - intro xa. simpl. apply hinhpr. exists (pr2 xa). apply idpath. - intros xa yb. unfold R. simpl. apply hinhfun. intro eq1. induction eq1 as [ x1 eq1 ]. exists x1. induction x1 as [ x1 isx1 ]. simpl. apply (!eq1). Qed.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.