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 …