proposition: Lemma iscommringcarrier {X : commring} (A : @subring X) : iscommringops (@op1 A) (@op2 A).
proof: Proof. intros. split with (isringcarrier A). apply (pr2 (@isabmonoidcarrier (ringmultabmonoid X) (multsubmonoid A))). Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids