exact Nat.pow_lt_pow_of_lt_left hc zero_lt_two
case intro.intro.intro.intro.intro.intro.refine'_2.calc_1
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' : ℤ√(-3) := { re := c, im := d }
⊢ (2 * Int.natAbs c) ^ 2 < Int.natAbs x ^ 2
no goals