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