Here's my understanding of the Nimbers and of your question. Actually, you'll see that I do need to beg the question somewhere, but since you do know a proof of the bitxor rule, perhaps that's allowed --- then my answer can be understood as a proof that your proof implies your proof is natural. (Said that way it sounds like an application of [Lob's theorem](http://www.yudkowsky.net/assets/44/LobsTheorem.pdf), or perhaps a converse....) By "Nimbers" I mean Nim games with Conway's game addition (put two games next two each other; on your turn, you choose one of the two boards to play on) modulo the second-player-win Games. By definition, a "game" is one where you lose when you cannot make a turn. The Nimbers are the classes of single-column Nim games. The zeroth observation is that addition (henceforth "$+$") is commutative, and that for any game $g$, the game $-g$ in which the roles are reversed is its inverse. The first observation, then, is that impartial games, and multi-column Nim games in particular, are 2-torsion: for any Nim game $g$, we have $g + g = g$. Thus the group generated by the Nimbers is a vector space over $\mathbb F_2$. The next ingredient I don't really have an a priori reason for, which is that the sum of any two Nimbers is a Nimber. Actually, proving this is probably just about the same as finding the bitxor formula, so perhaps my whole story is question-begging. But let's assume that this second ingredient is just an "observation". The third observation is the following. Let $G_k$ denote the group generated by the Nimbers $1,\dots,k$. If you allow the second observation, then it is not hard to see that if $n \in G_k$, then for every $m < n$, $m\in G_k$. Indeed, if $n\in G_k$, then I can write $n = \sum a_i$ for some sum of Nimbers with $a_i \leq k$. Let's play the game $n + \sum a_i$, which is a second-player win by assumption. Being magnanimous, I'll go first. On my turn I turn $n$ into $m$. Now you definitely have a move the return the sum to $0$. It definitely doesn't involve the pile I touched, so it must involve dropping one of the $a_i$s to an $a_i' < a_i$. But $a_i$ was one of our generators in $1,\dots,k$, and so $a_i'$ is also one of those generators. Now we can put the observations together to describe the structure of the Nimbers. We have $G_0 = \{0\}$ and $G_1 = \{0,1\}$ is the group of order $2$. By induction, the set of Nimbers $G = \{0,1,\dots,2^k-1\}$ is closed under Nimber addition. Consider $G_{2^k}$. It is an $\mathbb F_2$-vector space generated by $G$, which has $2^k$ elements, and by one more element. Thus $|G_{2^k}| = 2^{k+1}$. Thus $G_{2^k} = \{0,\dots,2^{k+1}-1\}$. The induction can then continue. So the Nimbers are naturally organized as an $\mathbb N$-filtered $\mathbb F_2$-vector space: $$\{0\} \subset \{0,1\} \subset \{0,1,2,3\} \subset \{0,1,2,3,4,5,6,7\} \subset \dots \subset \{0,\dots,2^{k-1}\} \subset \dots.$$ This doesn't completely pin down the addition, but it makes bitxor seem very likely. For example, it implies that if $m,n \in \{2^{k-1},\dots,2^k-1\}$, so that they have the same leading digit mod $2$, then their sum $m+n < 2^{k-1}$, and on the other hand if $m < 2^{k-1}$ and $n \in \{2^{k-1},\dots,2^k-1\}$, then $m+n \in \{2^{k-1},\dots,2^k-1\}$. This gives the bitxor rule in the leading digit. Of course, this analysis still allows lots of group structures on $\{0,\dots,2^k-1\}$. The rule is only that the structure has to extend the one on $\{0,\dots,2^{k-1}-1\}$. You can write down ad hoc group structures by twisting the given one by any permutation of $\{2^{k-1},\dots,2^k-1\}$. To completely pin down the bitxor group law requires playing a bit more with the third observation, I think. Let's see if we can do it. We know that the bitxor rule applies to Nimbers $N < 2^k$, by induction. We also know that $2^k + 2^k = 0$, so it applies to $N \leq 2^k$. To prove the claim, it suffices to prove that the Nimber of height $2^k+2^j$ for $j<k$ is equal to the Nim addition $2^k + 2^j$. Everything else will follow from linear algebra. But now all I need to do is to tell you a second-player-win strategy for the three-column Nim game with heights $2^j$, $2^k$, and $2^k+2^j$. Well, let's suppose you play on column $2^j$. Then I have such a strategy by induction in $j$ (and linear algebra). Suppose you play on column $2^k$. Then you make it into something in $\{0,\dots,2^k-1\}$, and adding $2^j$ keeps me in that group, so I just need to drop the column of height $2^k+2^j$ to match. Finally, suppose you play on column $2^k+2^j$. If you leave it above $2^k$, I'll play on column $2^j$ to match, and use induction in $j$ to know that that works. If you take it below height $2^k$, I'll drop the $2^k$-column to make the sum come out, using bitxor in the group $\{0,\dots,2^k-1\}$. Perhaps this is the proof you already know. It certainly is a follow-your-nose proof.