have hf : ∀ n, n ≤ f n := fun n => h' n n rfl.le
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
h' : ∀ (k n : ℕ), k ≤ n → k ≤ f n
⊢ ∀ (n : ℕ), f n = n
f : ℕ → ℕ
h : ∀ (n : ℕ), f (f n) < f (n + 1)
h' : ∀ (k n : ℕ), k ≤ n → k ≤ f n
hf : ∀ (n : ℕ), n ≤ f n
⊢ ∀ (n : ℕ), f n = n