Lemma isrigcarrier {X : rig} (A : subrig X) : isrigops (@op1 A) (@op2 A). Proof. intros. split. - exists (isabmonoidcarrier (rigaddsubmonoid A) ,, ismonoidcarrier (rigmultsubmonoid A)). + split. * intro a. apply (invmaponpathsincl _ (isinclpr1carrier A)). simpl. apply rigmult0x. * intro a. apply (invmaponpathsincl _ (isinclpr1carrier A)). simpl. apply rigmultx0. - split. * intros a b c. apply (invmaponpathsincl _ (isinclpr1carrier A)). simpl. apply rigldistr. * intros a b c. apply (invmaponpathsincl _ (isinclpr1carrier A)). simpl. apply rigrdistr. Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.