constructor
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
⊢ Associated' x A ↔ x = A ∨ x = star A
case mp
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
⊢ Associated' x A → x = A ∨ x = star A

case mpr
x A : ℤ√(-3)
hx : 0 ≤ x.re
hA : 0 ≤ A.re
⊢ x = A ∨ x = star A → Associated' x A