have bound : Complex.normSq (a / b - nearestℤω (a / b)) < 1 :=
  norm_sub_nearestℤω_self_lt (a / b : ℂ)
a b c : ℤω
h : b ≠ 0
⊢ ↑normSq (↑inclusion a - ↑inclusion b * ↑inclusion (nearestℤω (↑inclusion a / ↑inclusion b))) < ↑normSq (↑inclusion b)
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
⊢ ↑normSq (↑inclusion a - ↑inclusion b * ↑inclusion (nearestℤω (↑inclusion a / ↑inclusion b))) < ↑normSq (↑inclusion b)