Every normal subgroup of a finite group is contained in some composition series

Your approach has all the elements of a proof, but I wanted to offer suggestions for a "less messy" version.

First of all, as long as you are using that "any finite group has a composition series", you shouldn't need your lemma.

You could go about it this way. Let $H$ be a normal subgroup of $G$. Then $H$ has a composition series $1=H_0<\dots<H_k=H$. The group $G/H$ also has a composition series, which we will enumerate this way:

$$ H/H=H_{k}/H<\dots <H_n/H=G/H $$

By an isomorphism theorem, the fact that $(H_{j}/H)/(H_{j-1}/H)$ is simple is equivalent to $H_j/H_{j-1}$ being simple.

Putting these two chains together, you have that $H_0<\dots <H_n$ is a composition series for $G$ through $H$.

Yes your proof is essentially correct. You can make it look less messy as follows. Noticing that the proof that $G$ has a composition series in the first place has the same structure as your proof, you could do a two-in-one-blow induction on the order of $G$ by showing: "$G$ has a composition series, and if $H$ is a nontrivial proper normal subgroup of $G$, then it can be chosen to pass through $H$".

The base cases are $G$ trivial or simple, and the statement is obvious then (the second part is vacuously satisfied). Otherwise there exists a nontrivial proper normal subgroup $H$ of $G$; choose it, or for the second part take the one that is imposed. Now by induction $H$ has a composition series, which we stick below $H$ as part of our final composition series. The quotient $G/H$ also has a composition series, which we "lift" by taking the preimage in $G$ (under the projection modulo $H$) of every subgroup in the series to obtain the part of our composition series between $G$ and $H$, by the isomorphism theorem.