set c' : ℤ√(-3) := ⟨c, d⟩
case intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
⊢ ∃ c m, a = c + m * ↑x ∧ c.norm < 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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
c' : ℤ√(-3) := { re := c, im := d }
⊢ ∃ c m, a = c + m * ↑x ∧ c.norm < x ^ 2