theorem Nat.lt_or_eq_of_lt {n : ℕ} {m : ℕ} (h : n < Nat.succ m) : n < m ∨ n = m

If n < m⁺, then n < m or n = m.