big_sepM2 and associated lemmas

Following big_sepL2 and big_sepM. Based on some code from @robbertkrebbers.

Would like to hear your comments and also add some helpful lemmas about this big op.