proposition: Lemma iscommringquot {X : commring} (R : @ringeqrel X) : iscommringops (@op1 (setwith2binopquot R)) (@op2 (setwith2binopquot R)).
proof: Proof. intros. split with (isringquot R). apply (pr2 (@isabmonoidquot (ringmultabmonoid X) (ringmultmonoideqrel R))). Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids