dsimp
case a
a b c : ℤω
⊢ rt3 * ↑(negOfNat 1) * (↑(ofNat 1) / ↑2) =
    (-1 - { re := ↑(negOfNat 1) * (↑(ofNat 1) / ↑2), im := rt3 * (↑(ofNat 1) / ↑2) }).im
case a
a b c : ℤω
⊢ rt3 * ↑(negOfNat 1) * (↑1 / 2) = -0 - rt3 * (↑1 / 2)