apply Nat.succ_le_of_lt
case succ
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
k : ℕ
h_ind : ∀ (n : ℕ), k ≤ n → k ≤ f n
n : ℕ
hk : k + 1 ≤ n
⊢ k + 1 ≤ f n
case succ.h
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
k : ℕ
h_ind : ∀ (n : ℕ), k ≤ n → k ≤ f n
n : ℕ
hk : k + 1 ≤ n
⊢ k < f n