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