d : ℤ
n m : ℤ√d
⊢ (n.re * m.re + d * n.im * m.im) * (n.re * m.re + d * n.im * m.im) -
      d * (n.re * m.im + n.im * m.re) * (n.re * m.im + n.im * m.re) =
    (n.re * n.re - d * n.im * n.im) * (m.re * m.re - d * m.im * m.im)
d : ℤ
n m : ℤ√d
⊢ norm (n * m) = norm n * norm m
simp only [norm, mul_im, mul_re]
no goals
d : ℤ
n m : ℤ√d
⊢ (n.re * m.re + d * n.im * m.im) * (n.re * m.re + d * n.im * m.im) -
      d * (n.re * m.im + n.im * m.re) * (n.re * m.im + n.im * m.re) =
    (n.re * n.re - d * n.im * n.im) * (m.re * m.re - d * m.im * m.im)
ring