simp only [Zsqrtd.norm_def, hc, hd]
case h
a : ℤ√(-3)
heven : Even a.norm
c : ℤ
hc : a.re = c + c
d : ℤ
hd : a.im = d + d
⊢ a.norm = 4 * { re := c, im := d }.norm
case h
a : ℤ√(-3)
heven : Even a.norm
c : ℤ
hc : a.re = c + c
d : ℤ
hd : a.im = d + d
⊢ (c + c) * (c + c) - -3 * (d + d) * (d + d) = 4 * (c * c - -3 * d * d)