have : a.re = 0 := by rwa [← Int.abs_lt_one_iff]
case H.inl
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
⊢ Zsqrtd.norm a ≠ 1
case H.inl
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this : a.re = 0
⊢ Zsqrtd.norm a ≠ 1