fact: Definition commrigquot {X : commrig} (R : @rigeqrel X) : commrig := make_commrig (setwith2binopquot R) (iscommrigquot R).
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids