have : |(2⁻¹ : ℝ)| = 1 / 2 := by
  simp only [one_div, abs_eq_self, inv_nonneg, zero_le_bit0, zero_le_one]
a b c : ℤω
x : ℝ
bound : |x - ↑(round x)| ≤ 1 / 2
⊢ |x - ↑(round x)| ≤ |2⁻¹|
a b c : ℤω
x : ℝ
bound : |x - ↑(round x)| ≤ 1 / 2
this : |2⁻¹| = 1 / 2
⊢ |x - ↑(round x)| ≤ |2⁻¹|