obtain ⟨c, m, rfl, h2⟩ := Zqrtd.factor_div a hodd
a : ℤ√(-3)
x : ℤ
hodd : Odd x
h : 1 < |x|
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
⊢ ∃ c m, a = c + m * ↑x ∧ c.norm < x ^ 2 ∧ c ≠ 0 ∧ ∃ y, c.norm = x * y ∧ y.natAbs < x.natAbs
case intro.intro.intro
x : ℤ
hodd : Odd x
h : 1 < |x|
c m : ℤ√(-3)
h2 : c.norm < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ (c + m * ↑x).norm
⊢ ∃ c_1 m_1, c + m * ↑x = c_1 + m_1 * ↑x ∧ c_1.norm < x ^ 2 ∧ c_1 ≠ 0 ∧ ∃ y, c_1.norm = x * y ∧ y.natAbs < x.natAbs