have : (a / b : ℂ) - nearestℤω (a / b) = (a - nearestℤω (a / b) * b) * b⁻¹ :=
  by
  ring_nf
  have : (b : ℂ) * (b : ℂ)⁻¹ = 1 := by
    apply mul_inv_cancel
    simpa [coe_eq_zero] using h
  congr
  rw [mul_comm (b : ℂ)]
  rw [_root_.mul_assoc]
  rw [this]
  rw [_root_.mul_one]
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)
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
this :
  OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
      OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) =
    (OneHom.toFun (↑↑inclusion) a -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) *
          OneHom.toFun (↑↑inclusion) b) *
      sorryAx ℂ true
⊢ ↑normSq (↑inclusion a - ↑inclusion b * ↑inclusion (nearestℤω (↑inclusion a / ↑inclusion b))) < ↑normSq (↑inclusion b)