rw [Int.odd_iff_not_even, Int.odd_iff_not_even]
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
⊢ Odd a.re ∧ Odd a.im
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even a.norm
⊢ ¬Even a.re ∧ ¬Even a.im