doc(set_theory/game/nim): update module docs (#15406)

We update the module docs to reflect that you should use `to_left_moves_nim` and `to_right_moves_nim` to interface with the nim API, instead of using the raw definition (which has the problems the old docs mentioned).

src/set_theory/game/nim.lean

@@ -19,18 +19,15 @@ where `n` and `m` are natural numbers, then `G + H` has the Grundy value `n xor
 
 ## Implementation details
 
-The pen-and-paper definition of nim defines the possible moves of `nim o` to be `{o' | o' < o}`.
+The pen-and-paper definition of nim defines the possible moves of `nim o` to be `set.Iio o`.
 However, this definition does not work for us because it would make the type of nim
 `ordinal.{u} → pgame.{u + 1}`, which would make it impossible for us to state the Sprague-Grundy
 theorem, since that requires the type of `nim` to be `ordinal.{u} → pgame.{u}`. For this reason, we
-instead use `o.out.α` for the possible moves, which makes proofs significantly more messy and
-tedious, but avoids the universe bump.
-
-The lemma `nim_def` is somewhat prone to produce "motive is not type correct" errors. If you run
-into this problem, you may find the lemmas `exists_ordinal_move_left_eq` and `exists_move_left_eq`
-useful.
-
+instead use `o.out.α` for the possible moves. You can use `to_left_moves_nim` and
+`to_right_moves_nim` to convert an ordinal less than `o` into a left or right move of `nim o`, and
+vice versa.
 -/
+
 universes u
 
 /-- `ordinal.out'` has the sole purpose of making `nim` computable. It performs the same job as