Definition natlthtoleh (m n : nat) : m < n -> m ≤ n. Proof. intros r. unfold natleh. unfold natlth in r. generalize r. clear r. generalize m. clear m. induction n as [|n N]. - intros ? r. contradicts r (negnatgth0n m). - intros ? r. induction m as [|m _]. + apply natgthsn0. + change (S n > S m) with (n > m) in r. change (S (S n) > S m) with (S n > m). apply N. assumption. Defined.