obtain ⟨n, d, hb, hd⟩ := Int.factor_div a.im x hodd
case intro.intro.intro
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
⊢ ∃ c m, a = c + m * ↑x ∧ Zsqrtd.norm c < x ^ 2
case intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
⊢ ∃ c m, a = c + m * ↑x ∧ Zsqrtd.norm c < x ^ 2