rw [abs_eq_abs] at hre him
x y : ℤ√(-3)
hre : abs x.re = abs y.re
him : abs x.im = abs y.im
⊢ Associated' x y
x y : ℤ√(-3)
hre : x.re = y.re ∨ x.re = -y.re
him : x.im = y.im ∨ x.im = -y.im
⊢ Associated' x y