apply lt_of_le_of_ne _ (Spts.not_two _).symm
a : ℤ√(-3)
h2 : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 2 < Zsqrtd.norm a
a : ℤ√(-3)
h2 : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 2 ≤ Zsqrtd.norm a