Lemma iscommringcarrier {X : commring} (A : @subring X) : iscommringops (@op1 A) (@op2 A). Proof. intros. exists (isringcarrier A). apply (pr2 (@isabmonoidcarrier (ringmultabmonoid X) (multsubmonoid A))). Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.