rw [← coe_neg]
a b c : ℤω
⊢ OneHom.toFun (↑↑inclusion) (a + -b) = OneHom.toFun (↑↑inclusion) a + -OneHom.toFun (↑↑inclusion) b
a b c : ℤω
⊢ OneHom.toFun (↑↑inclusion) (a + -b) = OneHom.toFun (↑↑inclusion) a + OneHom.toFun (↑↑inclusion) (-b)