rw [him, MulZeroClass.mul_zero, sub_zero, ← Int.natAbs_mul_self, ← sq]
case inl
a : ℤ√(-3)
him : a.im = 0
⊢ a.re * a.re - -3 * a.im * a.im ≠ 2
case inl
a : ℤ√(-3)
him : a.im = 0
⊢ ↑(a.re.natAbs ^ 2) ≠ 2