Lemma natgthtogehsn (n m : nat) : n > m -> n ≥ (S m). Proof. revert m. induction n as [ | n IHn ]. - intros m X. induction (negnatgth0n _ X). - intros m X. destruct m as [ | m ]. + apply (natgehn0 n). + apply (IHn m X). Defined.