Upstream more big_op lemmas from Perennial
Perennial has a bunch of big_op lemmas at https://github.com/mit-pdos/perennial/tree/master/src/algebra/big_op. At least some of those are certainly worth upstreaming, but I find it hard to figure out where to draw the line.