proposition: Lemma isringquot {X : ring} (R : @ringeqrel X) : isringops (@op1 (setwith2binopquot R)) (@op2 (setwith2binopquot R)).
proof: Proof. intros. split with (make_dirprod (isabgrquot (ringaddabgreqrel R)) (ismonoidquot (ringmultmonoideqrel R))). simpl. set (opp1 := @op1 (setwith2binopquot R)). set (opp2 := @op2 (setwith2binopquot R)). split. - unfold isldistr. apply (setquotuniv3prop R (λ x x' x'', make_hProp _ (setproperty (setwith2binopquot R) (opp2 x'' (opp1 x x')) (opp1 (opp2 x'' x) (opp2 x'' x'))))). intros x x' x''. apply (maponpaths (setquotpr R) (ringldistr X x x' x'')). - unfold isrdistr. apply (setquotuniv3prop R (λ x x' x'', make_hProp _ (setproperty (setwith2binopquot R) (opp2 (opp1 x x') x'') (opp1 (opp2 x x'') (opp2 x' x''))))). intros x x' x''. apply (maponpaths (setquotpr R) (ringrdistr X x x' x'')). Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids