proposition: Lemma iseqrelabmonoidfrac (X : abmonoid) (A : submonoid X) : iseqrel (hrelabmonoidfrac X A).
proof: Proof. intros. set (assoc := assocax X). set (comm := commax X). set (R := hrelabmonoidfrac X A). assert (symm : issymm R). { intros xa yb. unfold R. simpl. apply hinhfun. intro eq1. destruct eq1 as [ x1 eq1 ]. split with x1. destruct x1 as [ x1 isx1 ]. simpl. apply (pathsinv0 eq1). } assert (trans : istrans R). { unfold istrans. intros ab cd ef. simpl. apply hinhfun2. destruct ab as [ a b ]. destruct cd as [ c d ]. destruct ef as [ e f ]. destruct b as [ b isb ]. destruct d as [ d isd ]. destruct f as [ f isf ]. intros eq1 eq2. destruct eq1 as [ x1 eq1 ]. destruct eq2 as [ x2 eq2 ]. simpl in *. split with (@op A (tpair _ d isd) (@op A x1 x2)). destruct x1 as [ x1 isx1 ]. destruct x2 as [ x2 isx2 ]. destruct A as [ A ax ]. simpl in *. rewrite (assoc a f (d + (x1 + x2))). rewrite (comm f (d + (x1 + x2))). destruct (assoc a (d + (x1 + x2)) f). destruct (assoc a d (x1 + x2)). destruct (assoc (a + d) x1 x2). rewrite eq1. rewrite (comm x1 x2). rewrite (assoc e b (d + (x2 + x1))). rewrite (comm b (d + (x2 + x1))). destruct (assoc e (d + (x2 + x1)) b). destruct (assoc e d (x2 + x1)). destruct (assoc (e + d) x2 x1). destruct 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). destruct (assoc (c + b) f (x2 + x1)). destruct (assoc (c + f) b (x2 + x1)). rewrite (assoc c b f). rewrite (assoc c f b). rewrite (comm b f). apply idpath. } assert (refl : isrefl R). { intro xa. simpl. apply hinhpr. split with (pr2 xa). apply idpath. } apply (iseqrelconstr trans refl symm). Defined.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders