have h2 : 2 < a.norm := by
  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 : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ ∃ u q,
    0 ≤ q.re ∧
      q.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm q) ∧ a = q * u ∧ IsCoprime u.re u.im ∧ Zsqrtd.norm u < Zsqrtd.norm a
a : ℤ√(-3)
h2✝ : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < Zsqrtd.norm a
⊢ ∃ u q,
    0 ≤ q.re ∧
      q.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm q) ∧ a = q * u ∧ IsCoprime u.re u.im ∧ Zsqrtd.norm u < Zsqrtd.norm a