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.