have := abs_mul (c⁻¹ * x - round (c⁻¹ * x)) c
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |(c⁻¹ * x - ↑(round (c⁻¹ * x))) * c| = |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c|
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c