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