have hfn := hf n
m✝ : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m✝ + 1)
n m : ℕ
hnm : f n = f m
⊢ n = m
m✝ : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m✝ + 1)
n m : ℕ
hnm : f n = f m
hfn : f (f n) = n + (2 * m✝ + 1)
⊢ n = m