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