calc
  k ≤ f (f (n - 1)) := h_ind _ (h_ind (n - 1) (le_tsub_of_add_le_right hk))
  _ < f n := tsub_add_cancel_of_le (le_trans (Nat.succ_le_succ (Nat.zero_le _)) hk) ▸ h _
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
no goals