Add `big_sepL2_app_inv_2`.

This is a useful lemma (at least for me), and I don't think it's directly derivable from the other two _inv lemmas.