revert n_ih
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
n_ih : f ((n + 1) * f 1) = n + 1 ∨ f 1 = 0
⊢ f ((n + 1) * f 1) = n + 1
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
⊢ f ((n + 1) * f 1) = n + 1 ∨ f 1 = 0 → f ((n + 1) * f 1) = n + 1