proposition: Lemma commringfraccomm1 (X : commring) (S : @subabmonoid (ringmultabmonoid X)) : iscomm (commringfracop1 X S).
proof: 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. destruct xs as [ x s ]. destruct s as [ s iss ]. destruct xs' as [ x' s' ]. destruct s' as [ s' iss' ]. simpl. apply pathsdirprod. - change (paths ((s' * x) + (s * x')) ((s * x') + (s' * x))). destruct (ringcomm1 X (s' * x) (s * x')). apply idpath. - apply (invmaponpathsincl _ (isinclpr1carrier (pr1 S))). simpl. change (paths (s * s') (s' * s)). apply (ringcomm2 X). Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids