calc
  p.re ^ 2 = p.re ^ 2 + 3 * p.im ^ 2 - 3 := by simp [hq]
  _ = p.norm - 3 := by
    rw [Zsqrtd.norm_def]
    ring
  _ = 1 := by
    rw [hfour]
    norm_num
p : ℤ√(-3)
hfour : p.norm = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ p.re ^ 2 = 1
no goals