have hparity : Even a.re ↔ Even a.im := by
  have : ¬ Even (3 : ℤ) := by decide
  simpa [this, two_ne_zero, Zsqrtd.norm_def, parity_simps] using heven
a : ℤ√(-3)
heven : Even a.norm
⊢ ∃ b, a.norm = 4 * b.norm
a : ℤ√(-3)
heven : Even a.norm
hparity : Even a.re ↔ Even a.im
⊢ ∃ b, a.norm = 4 * b.norm