have hc : c * c⁻¹ = 1 := by
  apply mul_inv_cancel
  exact ne_of_gt c_pos
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c