proposition: Lemma natnonzerocomm (a b : natnonzero) : (@op natnonzero a b) = (@op natnonzero b a).
proof: Proof. intros. apply (invmaponpathsincl _ (isinclpr1carrier _) (@op natnonzero a b) (@op natnonzero b a)). simpl. apply natmultcomm. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Archimedean UniMath.Algebra.Domains_and_Fields UniMath.Algebra.IteratedBinaryOperations