Misere Nim rigurous proof

Question

I know that this is the optimal strategy for misere nim game:

When played as a misère game, Nim strategy is different only when the normal play move would leave only heaps of size one. In that case, the correct move is to leave an odd number of heaps of size one (in normal play, the correct move would be to leave an even number of such heaps).

My question is, what is the rigorous proof that the winning player is the first to have the occasion to "leave an odd number of heaps of size one" ? Why cannot the second player do this ? I mean ok it's clear I can not have this: 2 1 1 1 1 1 and second player's turn cause XOR sum is not 0 (and intuitively as the number of stones becomes smaller and smaller I feel that there is a point where I have k heaps of size 1 and k >= 0 and one of size > 1 and first player's turn; but why exactly is there a point when k piles are of size 1 and another one of size > 1? It seems obvious but It breaks my mind) but I can not figure out something very rigorous and I would like a more formal proof.

Answer 1

Let's call a heap "big" if it has size greater than $1$.

After each move, the number of big heaps either stays the same (when a heap of size $1$ is removed or a big heap is reduced to a smaller big heap), or decreases by one (when a big heap is reduced to size $1$ or $0$). And if there is at last one big heap, the number of big heaps can't stay the same forever since the game will end (no big heaps then) as the number of stones always decreases.

Since the number of big heaps always ends up decreasing by $1$ at a time, we'll end up with just $1$ big heap eventually. At that point, the "XOR sum" is nonzero since the big heap has a bit not in the ones place. Also at that point, the player to move can choose how many heaps of size $1$ to leave.