Lemma natnonzerocomm (a b : natnonzero) : (@op natnonzero a b) = (@op natnonzero b a). Proof. intros. apply (invmaponpathsincl _ (isinclpr1carrier _) (@op natnonzero a b) (@op natnonzero b a)). simpl. apply natmultcomm. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.NegativePropositions.