apply even_iff_two_dvd.mpr (dvd_trans _ hdvd)
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : 4 ∣ a.norm
hq : p.im ≠ 0
hp : p.norm = 4
⊢ Even a.norm
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : 4 ∣ a.norm
hq : p.im ≠ 0
hp : p.norm = 4
⊢ 2 ∣ 4