It is not true in general that the image of $ds$ is contained in the horizontal space. Let us consider a simple example. Let $E=\mathbb{R}^2$, $M=\mathbb{R}$, and $\pi$ be the projection on the first coordinate. In other words, $E$ is the trivial line bundle over the real line. Let $\nabla$ be the trivial connection, that is, the horizontal space at any point $(x,y)\in E$ is spanned by $\partial/\partial x$. In this setting, any section is given by$$x\mapsto(x,f(x)),$$and a section is horizontal (the image of its differential is contained in the horizontal space at any point) if and only if the function $f$ is constant.
Edit: A few words about the Leibniz rule. There are numerous ways to think about connections and the Leibniz rule, and I guess they are all the same in a way. Here is one of those ways.
Let $p\in M$ and $w\in T_pM$. We want to show that for a section $s$ and a function $f$ we have $$\nabla_wfs=df(w)s+f\nabla_ws.$$We proceed by the following steps.
1) Let $e_1,\ldots,e_k$ be a local trivialization of $E$ around $p$, and suppose first that $\nabla$ is the corresponding trivial covariant derivative. In this case, the Leibniz rule is just the usual one for paths in Euclidean space.
Note that step 1) is not enough, as most of the connections do not look locally like a trivial connection.
2)Let $\rho,\rho'$ be two different projections on the vertical bundle, each one of which respects the linear structure of $E$, and let $\nabla,\nabla'$ denote the corresponding covariant derivatives, respectively. We claim that the difference $\nabla-\nabla'=:T$ is a tensor. That is, the map$$(X,s)\mapsto T(X,s)=\nabla_Xs-\nabla_X's$$ is $C^\infty(M)$-linear in both parameters. To see this, let $\widetilde{X}$ and $\widetilde{X}'$ be horizontal lifts of $X$ with respect to both connections. Then $$T(X,s)=\nabla_Xs-\nabla_X's=\left(ds(X)-\widetilde{X}\right)-\left(ds(X)-\widetilde{X}'\right)=\widetilde{X}-\widetilde{X}'.$$ In other words, $T(X,s)$ does not depend on the derivative of $s$ but only on the value of $s$ at a point, and the claim follows.
3) Finally, we claim that if $\nabla$ and $\nabla'$ are two covarivant derivatives, such that $\nabla-\nabla'$ is a tensor and $\nabla'$ satisfies the Leibniz rule, then so does $\nabla$. This is a nice exercise for anyone who is new to connections.
The full Leibniz rule follows from the above three steps.