rw [even_iff_two_dvd, even_iff_two_dvd]
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
this : Even a.re ↔ Even a.im
⊢ ¬(Even a.re ∧ Even a.im)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
this : Even a.re ↔ Even a.im
⊢ ¬(2 ∣ a.re ∧ 2 ∣ a.im)