Lemma isringquot {X : ring} (R : @ringeqrel X) : isringops (@op1 (setwith2binopquot R)) (@op2 (setwith2binopquot R)). Proof. intros. exists (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.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.