feat(algebra/big_operators/finprod): add a few lemmas (#8261)
* add `finprod_eq_single` and `finsum_eq_single`;
* add `finprod_induction` and `finsum_induction`;
* add `single_le_finprod` and `single_le_finsum`;
* add `one_le_finprod'` and `finsum_nonneg`.
