Definition natminuslthn (n m : nat) (is : n > 0) (is' : m > 0) : n - m < n. Proof. revert m is is'. induction n as [ | n IHn ]. - intros. induction (negnatgth0n _ is). - intro m. induction m. + intros. induction (negnatgth0n _ is'). + intros. apply (natlehlthtrans _ n _). * apply (natminuslehn n m). * apply natlthnsn. Defined.