ring
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
⊢ (p.re * a.im - a.re * p.im) * (p.re * a.im + a.re * p.im) =
    a.im ^ 2 * (p.re * p.re - -3 * p.im * p.im) - p.im ^ 2 * (a.re * a.re - -3 * a.im * a.im)
no goals