apply step2 hcoprime hdvd hpprime
case inr.intro
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : Zsqrtd.norm p ∣ Zsqrtd.norm a
hq : p.im ≠ 0
hpprime : Prime (Zsqrtd.norm p)
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ Zsqrtd.norm a = Zsqrtd.norm p * Zsqrtd.norm u
no goals