have h2 : 2 < a.norm.natAbs := by
  zify
  rw [abs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) a)]
  apply lt_of_le_of_ne _ (Spts.not_two _).symm
  rw [← one_mul (2 : ℤ), mul_two, Int.add_one_le_iff]
  apply lt_of_le_of_ne _ h2.symm
  rw [← Int.sub_one_lt_iff, sub_self]
  exact Spts.pos_of_coprime' hcoprime
a : ℤ√(-3)
h2 : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ ∃ u q, 0 ≤ q.re ∧ q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
⊢ ∃ u q, 0 ≤ q.re ∧ q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm