rw [← one_mul (2 : ℤ), mul_two, Int.add_one_le_iff]
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
⊢ 1 < Zsqrtd.norm a