simp only [Zsqrtd.norm_def, hc, hd]
case inl.intro.intro.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
c : ℤ
hc : a.re = c + c
d : ℤ
hd : a.im = d + d
⊢ Zsqrtd.norm a = 4 * Zsqrtd.norm { re := c, im := d }
case inl.intro.intro.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
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)