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.