rw [← sq_abs]
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this✝ : a.re = 0
hb : ¬a.im = 0
this : 1 ≤ abs a.im
⊢ 1 ≤ a.im ^ 2
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this✝ : a.re = 0
hb : ¬a.im = 0
this : 1 ≤ abs a.im
⊢ 1 ≤ abs a.im ^ 2