ext
a b c : ℤω
x y : ℤ
⊢ ↑x + ↑y * { re := -1 / 2, im := rt3 / 2 } = { re := ↑x - ↑y / 2, im := ↑y * rt3 / 2 }
case a
a b c : ℤω
x y : ℤ
⊢ (↑x + ↑y * { re := -1 / 2, im := rt3 / 2 }).re = { re := ↑x - ↑y / 2, im := ↑y * rt3 / 2 }.re

case a
a b c : ℤω
x y : ℤ
⊢ (↑x + ↑y * { re := -1 / 2, im := rt3 / 2 }).im = { re := ↑x - ↑y / 2, im := ↑y * rt3 / 2 }.im