feat(data/list/basic): list products (#10184)
Adding a couple of lemmas about list products. The first is a simpler variant of `head_mul_tail_prod'` in the case where the list is not empty. The other is a variant of `list.prod_ne_zero` for `list ℕ`.
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
