fact: Definition carrierofasubcommrig {X : commrig} (A : @subrig X) : commrig := make_commrig A (iscommrigcarrier A).
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids