obtain ⟨f, hf⟩ := hdvd
a p : ℤ√(-3)
hdvd : p.norm ∣ a.norm
hpprime : Prime p.norm
⊢ ∃ u, a = p * u ∨ a = star p * u
case intro
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
⊢ ∃ u, a = p * u ∨ a = star p * u