This is a continuation of this previous post covering a formalization of impartial games. In this post, I will define the game of Nim, and use it to state and prove the Sprague-Grundy theorem.
Defining Nim
I chose to define Nim in terms of the BinNat.N type rather than …