proposition: Lemma iscommcarrier {X : abmonoid} (A : submonoid X) : iscomm (@op A).
proof: Proof. intros a a'. apply (invmaponpathsincl _ (isinclpr1carrier A)). simpl. apply (pr2 (pr2 X)). Defined.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders