unfold nearestℤω
case mk
a b c : ℤω
x y : ℝ
⊢ |({ re := x, im := y } - OneHom.toFun (↑↑inclusion) (nearestℤω { re := x, im := y })).re| ≤ |2⁻¹|
case mk
a b c : ℤω
x y : ℝ
⊢ |({ re := x, im := y } -
          OneHom.toFun (↑↑inclusion)
            (let y_1 := round (2 * rt3⁻¹ * { re := x, im := y }.im);
            { x := round ({ re := x, im := y }.re + 2⁻¹ * ↑y_1), y := y_1 })).re| ≤
    |2⁻¹|