proposition: Lemma ismonoidcarrier {X : monoid} (A : submonoid X) : ismonoidop (@op A).
proof: Proof. split. - intros a a' a''. apply (invmaponpathsincl _ (isinclpr1carrier A)). simpl. apply (assocax X). - split with (make_carrier _ (unel X) (pr2 (pr2 A))). split. + simpl. intro a. apply (invmaponpathsincl _ (isinclpr1carrier A)). simpl. apply (lunax X). + intro a. apply (invmaponpathsincl _ (isinclpr1carrier A)). simpl. apply (runax X). Defined.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders