Lemma commringfracassoc1 (X : commring) (S : @subabmonoid (ringmultabmonoid X)) : isassoc (commringfracop1 X S). Proof. intros. set (R := eqrelcommringfrac X S). set (add1int := commringfracop1int X S). set (add1 := commringfracop1 X S). unfold isassoc. assert (int : ∏ (xs xs' xs'' : X × S), setquotpr R (add1int (add1int xs xs') xs'') = setquotpr R (add1int xs (add1int xs' xs''))). unfold add1int. unfold commringfracop1int. intros xs xs' xs''. apply (@maponpaths _ _ (setquotpr R)). simpl. apply pathsdirprod. - unfold pr1carrier. apply (commringfracl2 X (pr1 xs) (pr1 xs') (pr1 xs'') (pr1 (pr2 xs)) (pr1 (pr2 xs')) (pr1 (pr2 xs''))). - apply (invmaponpathsincl _ (isinclpr1carrier (pr1 S))). unfold pr1carrier. simpl. set (assoc2 := ringassoc2 X). apply (assoc2 (pr1 (pr2 xs)) (pr1 (pr2 xs')) (pr1 (pr2 xs''))). - apply (setquotuniv3prop R (λ x x' x'', _ = _)), int. Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.