Enable the use of the proofmode for proving big-op lemmas

There are many things that are painful about bi/big_op.v, but one of the biggest ones is the fact that we cannot use the proofmode to prove these lemmas -- because the proofmode actually uses big-ops itself.

It would be good to find some way to stratify this, so that only some core set of lemmas needs to be shown without the proofmode, and the rest can use the proofmode.