have f_injective : f.Injective := by
  intro n m hnm; have hfn := hf n; simp_all only [add_left_inj]
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
⊢ False
case intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
⊢ False