Lemma isasymmabmonoidfracrelint (X : abmonoid) (A : subabmonoid X) {L : hrel X} (is : ispartbinophrel A L) (isl : isasymm L) : isasymm (abmonoidfracrelint X A L). Proof. intros. set (assoc := (assocax X) : isassoc (@op X)). unfold isassoc in assoc. set (comm := commax X). unfold iscomm in comm. unfold isasymm. intros xa1 xa2. unfold abmonoidfracrelint. simpl. apply (@hinhuniv2 _ _ (make_hProp _ isapropempty)). intros t2l1 t2l2. set (c1a := pr1 t2l1). set (l1 := pr2 t2l1). set (c2a := pr1 t2l2). set (l2 := pr2 t2l2). set (c1 := pr1 c1a). set (c2 := pr1 c2a). set (x1 := pr1 xa1). set (a1 := pr1 (pr2 xa1)). set (x2 := pr1 xa2). set (a2 := pr1 (pr2 xa2)). assert (ll1 : L ((x1 + a2) + (@op X c1 c2)) ((x2 + a1) + (@op X c1 c2))). { induction (assoc (x1 + a2) c1 c2). induction (assoc (x2 + a1) c1 c2). apply ((pr2 is) _ _ _ (pr2 c2a)). apply l1. } assert (ll2 : L ((x2 + a1) + (@op X c1 c2)) ((x1 + a2) + (@op X c1 c2))). { induction (comm c2 c1). induction (assoc (x1 + a2) c2 c1). induction (assoc (x2 + a1) c2 c1). apply ((pr2 is) _ _ _ (pr2 c1a)). apply l2. } apply (isl _ _ ll1 ll2). Qed.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.