simp only [ofNat_eq_coe, Nat.cast_one, cast_one, Nat.cast_ofNat, one_div, cast_negOfNat, mul_neg,
  mul_one, neg_mul]
case mk
b c : ℤω
x y : ℤ
⊢ ↑x = ↑x + ↑y * (rt3⁻¹ * (↑(ofNat 1) / ↑2) * rt3) + ↑y * ↑(negOfNat 1) * (↑(ofNat 1) / ↑2)
case mk
b c : ℤω
x y : ℤ
⊢ ↑x = ↑x + ↑y * (rt3⁻¹ * 2⁻¹ * rt3) + -(↑y * 2⁻¹)