rw [← Int.sub_one_lt_iff, sub_self]
a : ℤ√(-3)
h2 : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 1 ≤ Zsqrtd.norm a
a : ℤ√(-3)
h2 : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 0 < Zsqrtd.norm a