have hneg1 : 1 ≤ a.norm := by
  rw [← Int.sub_one_lt_iff, sub_self]
  apply lt_of_le_of_ne (Zsqrtd.norm_nonneg (by norm_num) a)
  rw [Ne, eq_comm, Zsqrtd.norm_eq_zero_iff (by norm_num : (-3 : ℤ) < 0)]
  rintro rfl
  rw [Zsqrtd.zero_im, Zsqrtd.zero_re] at hcoprime
  exact not_isCoprime_zero_zero hcoprime
case h
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ a.norm
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
⊢ ∃ c, |x| = c.norm
case h
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ a.norm
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
hneg1 : 1 ≤ a.norm
⊢ ∃ c, |x| = c.norm