simp only [complexω]
case a
a b c : ℤω
⊢ complexω.re * complexω.im + complexω.im * complexω.re = (-complexω - 1).im
case a
a b c : ℤω
⊢ -1 / 2 * (rt3 / 2) + rt3 / 2 * (-1 / 2) = (-{ re := -1 / 2, im := rt3 / 2 } - 1).im