rw [Zsqrtd.norm_def]
p : ℤ√(-3)
hfour : p.norm = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ p.re ^ 2 + 3 * p.im ^ 2 - 3 = p.norm - 3
p : ℤ√(-3)
hfour : p.norm = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ p.re ^ 2 + 3 * p.im ^ 2 - 3 = p.re * p.re - -3 * p.im * p.im - 3