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