apply lt_of_le_of_ne
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ 0 < Zsqrtd.norm a
case a
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ 0 ≤ Zsqrtd.norm a

case a
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ 0 ≠ Zsqrtd.norm a