add some big_opS lemmas

Merged Ralf Jung requested to merge ralf/big_opS into master

All proofs taken from Perennial (but I adjusted the names).

Merge request reports