Index: lib/doc/nim.txt
==================================================================
--- lib/doc/nim.txt
+++ lib/doc/nim.txt
@@ -29,10 +29,22 @@
     定理
       - G1≡*n1, ..., Gk≡*nk ならば、G={G1, ..., Gk} ≡ *mex(n1,...,nk)
         where mex(S) = min(nat \setminus S)
         帰納的に、全てのゲームはなんらかの *n と等価
 
+    定理の証明
+      - {G1, ..., Gk} は *mex(n1,...,nk) と等価。
+        つまり和を取ると必敗。
+        *mex(n1,...,nk) 側を動かした場合、相手は対応する Gi に遷移する。
+        {G} 側を mex(n1,...,nk) より小さいゲームに動かした場合、mex側を対応する値に変える。
+        {G} 側を mex より大きいゲームに動かした場合、その大きいゲームをmexに下げる。
+        で両側等価を保ててしまう。
+
+    等価(和を取ると必敗) => 勝ち負け一致 の証明
+      - 偶奇を考えれば良い。必勝ゲーム+必敗ゲーム なら初手で必勝を必敗に変えて常にその状態を
+        保てば勝てる。ゆえに一致しないなら和をとったゲームは必勝。
+
 
 おまけ
   @G を G のnim値とする。つまりG≡*@G
   G = X + Y ならば @G = @X xor @Y
   山が複数のnimの勝敗は全部xorとった1つ山のnimに等しいのと同じ原理。