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