apply_fun f
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
⊢ ¬f 1 = f 0
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
⊢ f (f 1) ≠ f (f 0)