Add lemmas `big_sepM2_inv_{l,r}` and rename `big_sepM2_lookup_{1,2}` into `big_sepM2_lookup_{l,r}`.

In !690 (merged) I noticed two things:

• The proof in !690 (merged) can be simplified using the new lemmas big_sepM2_inv_{l,r}, which generalize big_sepM2_lookup_{1,2}
• The lemmas big_sepM2_lookup_{1,2} are inconsistently named. For other lemmas, we use _l and _r, so I renamed them into big_sepM2_lookup_{l,r}.