proposition: Lemma isringcarrier {X : ring} (A : subring X) : isringops (@op1 A) (@op2 A).
proof: Proof. intros. split with (make_dirprod (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.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids