rw [this]
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ℤα (OneHom.toFun (↑↑inclusion) a / 0) = 0