Lemma isringcarrier {X : ring} (A : subring X) : isringops (@op1 A) (@op2 A). Proof. intros. exists (isabgrcarrier (addsubgr A) ,, ismonoidcarrier (multsubmonoid A)). split. - intros a b c. apply (invmaponpathsincl _ (isinclpr1carrier A)). simpl. apply ringldistr. - intros a b c. apply (invmaponpathsincl _ (isinclpr1carrier A)). simpl. apply ringrdistr. Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.