rw [rt3_sq]
case a
a b c : ℤω
⊢ ↑(ofNat 1) / ↑4 + rt3 ^ 2 * ↑(negOfNat 1) * (↑(ofNat 1) / ↑4) =
    (-1 - { re := ↑(negOfNat 1) * (↑(ofNat 1) / ↑2), im := rt3 * (↑(ofNat 1) / ↑2) }).re
case a
a b c : ℤω
⊢ ↑(ofNat 1) / ↑4 + 3 * ↑(negOfNat 1) * (↑(ofNat 1) / ↑4) =
    (-1 - { re := ↑(negOfNat 1) * (↑(ofNat 1) / ↑2), im := rt3 * (↑(ofNat 1) / ↑2) }).re