induction' k with k h_ind
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
k : ℕ
⊢ ∀ (n : ℕ), k ≤ n → k ≤ f n
case zero
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
⊢ ∀ (n : ℕ), 0 ≤ n → 0 ≤ f n

case succ
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
k : ℕ
h_ind : ∀ (n : ℕ), k ≤ n → k ≤ f n
⊢ ∀ (n : ℕ), k + 1 ≤ n → k + 1 ≤ f n