proposition: Lemma commringfracassoc1 (X : commring) (S : @subabmonoid (ringmultabmonoid X)) : isassoc (commringfracop1 X S).
proof: Proof. intros. set (R := eqrelcommringfrac X S). set (add1int := commringfracop1int X S). set (add1 := commringfracop1 X S). unfold isassoc. assert (int : ∏ (xs xs' xs'' : dirprod X S), paths (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. Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids