Lemma iscommrigquot {X : commrig} (R : @rigeqrel X) : iscommrigops (@op1 (setwith2binopquot R)) (@op2 (setwith2binopquot R)). Proof. intros. exists (isrigquot R). apply (pr2 (@isabmonoidquot (commrigmultabmonoid X) (multmonoideqrel R))). Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.