refactor(algebra/big_operators/basic): Reorder lemmas (#11113)
This PR does the following things:
- Move `prod_bij` and `prod_bij'` earlier in the file, so that they can be put to use.
- Move `prod_product` and `prod_product'` past `prod_sigma` and `prod_sigma'` down to `prod_product_right` and `prod_product_right'`.
- Use `prod_bij` and `prod_sigma` to give an easier proof of `prod_product`.
- The new proof introduces `prod_finset_product` and the remaining three analogs of the four `prod_product` lemmas.
`prod_finset_product` is a lemma that I found helpful in my own work.
