rw [Zsqrtd.norm_def]
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
⊢ a.im ^ 2 * p.norm - p.im ^ 2 * (p.norm * f) = p.norm * (a.im ^ 2 - p.im ^ 2 * f)
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
⊢ a.im ^ 2 * (p.re * p.re - -3 * p.im * p.im) - p.im ^ 2 * ((p.re * p.re - -3 * p.im * p.im) * f) =
    (p.re * p.re - -3 * p.im * p.im) * (a.im ^ 2 - p.im ^ 2 * f)