have : 1 ≤ a.im ^ 2 := by
  rw [← sq_abs]
  exact pow_le_pow_left zero_le_one this 2
case neg
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |a.re| < 1
this✝ : a.re = 0
hb : ¬a.im = 0
this : 1 ≤ |a.im|
⊢ 3 * a.im * a.im ≠ 1
case neg
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |a.re| < 1
this✝¹ : a.re = 0
hb : ¬a.im = 0
this✝ : 1 ≤ |a.im|
this : 1 ≤ a.im ^ 2
⊢ 3 * a.im * a.im ≠ 1