Definition natminuslthninv (n m : nat) (is : n - m < n) : m > 0. Proof. revert m is. induction n as [ | n IHn ]. - intros. induction (negnatlthn0 _ is). - intro m. destruct m as [ | m ]. + intro. induction (negnatlthnn _ is). + intro. apply (natgthsn0 m). Defined.