Lemma commringfraccomm1 (X : commring) (S : @subabmonoid (ringmultabmonoid X)) : iscomm (commringfracop1 X S). Proof. intros. set (R := eqrelcommringfrac X S). set (add1int := commringfracop1int X S). set (add1 := commringfracop1 X S). unfold iscomm. apply (setquotuniv2prop _ (λ x x', _ = _)). intros xs xs'. apply (@maponpaths _ _ (setquotpr R) (add1int xs xs') (add1int xs' xs)). unfold add1int. unfold commringfracop1int. induction xs as [ x s ]. induction s as [ s iss ]. induction xs' as [ x' s' ]. induction s' as [ s' iss' ]. simpl. apply pathsdirprod. - change (s' * x + s * x' = s * x' + s' * x). induction (ringcomm1 X (s' * x) (s * x')). apply idpath. - apply (invmaponpathsincl _ (isinclpr1carrier (pr1 S))). simpl. change (s * s' = s' * s). apply (ringcomm2 X). Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.