Lemma negnatgthtoleh {n m : nat} : ¬ (n > m) -> n ≤ m. Proof. unfold natleh. revert m. induction n as [|n N]. - intros m r. exact (natgthsn0 m). - intro m. change (S m > S n) with (m > n). induction m as [|m _]. + intro r. contradicts (natgthsn0 n) r. + change (S n > S m) with (n > m). intro r. exact (N m r). Defined.