have heven : Even a.norm :=
  by
  apply even_iff_two_dvd.mpr (dvd_trans _ hdvd)
  norm_num
case inl
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : 4 ∣ Zsqrtd.norm a
hq : p.im ≠ 0
hp : Zsqrtd.norm p = 4
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ Zsqrtd.norm a = 4 * Zsqrtd.norm u
case inl
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : 4 ∣ Zsqrtd.norm a
hq : p.im ≠ 0
hp : Zsqrtd.norm p = 4
heven : Even (Zsqrtd.norm a)
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ Zsqrtd.norm a = 4 * Zsqrtd.norm u