1/ You do not need the theorem that you mention, " if I have 2 numbers , and I know that one of them is not 0, and their product is 0, then necessarily the other number is 0". You don't need it because you want to prove that the product is 0, you are not in a situation where you want to use the fact that the product is zero.
So the theorem Zmult_integral_r is not useful for the lemma in this question. It would be useful if you had to prove forall l, product l = 0 -> contains_zero l = true.
Here, for your problem, the two functions that you consider are recursive, so the usual hint is to do a proof by induction, and then to use the tactic simpl to make the functions look simpler.