apply (iff_iff_and_or_not_and_not.mp this).resolve_left
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
⊢ ¬(Even a.re ∧ Even a.im)