nums1 is not an input, it is the output buffer: m real values followed by
n zero slots. Writing forward would clobber values you have not read yet, so you write
backwards — i at the last real value of nums1,
j at the last value of nums2, and a write cursor w
at the very end. The invariant w = i + j + 1 is the whole proof:
w is always strictly ahead of i, so a write can never
destroy an unread cell.
while (j >= 0) is mandatory — leftover nums2 values
have never been copied into the buffer at all. A matching while (i >= 0) loop is
not needed: leftover nums1 values are already sitting at indices
0..i, which is exactly where they belong.