rw [this, div_zero]
a b c : ℤω
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) 0) = 0
a b c : ℤω
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ nearestℤω 0 = 0