have : ¬ Even (3 : ℤ) := by decide
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
⊢ Even a.re ↔ Even a.im
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
this : ¬Even 3
⊢ Even a.re ↔ Even a.im