apply hpprime.dvd_or_dvd
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
⊢ p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
⊢ p.norm ∣ (p.re * a.im - a.re * p.im) * (p.re * a.im + a.re * p.im)