simp only [Zsqrtd.norm_def, this, MulZeroClass.zero_mul, zero_sub, neg_mul, neg_neg]
case inl
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |a.re| < 1
this : a.re = 0
⊢ a.norm ≠ 1
case inl
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |a.re| < 1
this : a.re = 0
⊢ 3 * a.im * a.im ≠ 1