rw [mul_assoc,mul_assoc,mul_comm rt3]
case mk
b c : ℤω
x y : ℤ
⊢ ↑x = ↑x + ↑y * rt3 * rt3⁻¹ * (↑(ofNat 1) / ↑2) + ↑y * ↑(negOfNat 1) * (↑(ofNat 1) / ↑2)
case mk
b c : ℤω
x y : ℤ
⊢ ↑x = ↑x + ↑y * (rt3⁻¹ * (↑(ofNat 1) / ↑2) * rt3) + ↑y * ↑(negOfNat 1) * (↑(ofNat 1) / ↑2)