How to prove the following properties of Small-step semantics?

Question

I have to prove the following 2 properties of the Small-step semantics of the WHILE programming language:

• If $\langle C_1; C_2, s\rangle \rightarrow^k s'$ then there is a state $s''$ and natural numbers $k_1$ and $k_2$ such that $\langle C_1;s \rangle \rightarrow^{k_1} s''$ and $\langle C_2; s'' \rangle \rightarrow^{k_2} s'$ where $k_1 + k_2 = k$.
• If $\langle C_1, s \rangle \rightarrow^k s'$ then $\langle C_1; C_2, s \rangle \rightarrow^k \langle C_2, s'\rangle$.

I am not quite sure which kind of induction I should use. I am not asking for a full proof, I would rather appreciate some hints on which kind of induction I should use in this case. Thanks in advance!