Add pair_op_1 and pair_op_2

The two new lemmas allow splitting the resources in one component of a pair when the other component has nothing. In combination with pair_split, they allow to arbitrarily split the resource (a ⋅ a', b ⋅ b').

This is in line with prod_local_update_1 and prod_local_update_2, the lemmas that allow, in a sense, to only consider one component of a pair.

This change was not discussed earlier, I just needed these lemmas in my own developments.