feat(set_theory/game/nim): recursors for left/right nim moves (#15408)

src/set_theory/game/nim.lean

@@ -96,6 +96,16 @@ lemma move_right_nim {o : ordinal} (i) :
   (nim o).move_right (to_right_moves_nim i) = nim i :=
 by simp
 
+/-- A recursion principle for left moves of a nim game. -/
+@[elab_as_eliminator] def left_moves_nim_rec_on {o : ordinal} {P : (nim o).left_moves → Sort*}
+  (i : (nim o).left_moves) (H : ∀ a < o, P $ to_left_moves_nim ⟨a, H⟩) : P i :=
+by { rw ←to_left_moves_nim.apply_symm_apply i, apply H }
+
+/-- A recursion principle for right moves of a nim game. -/
+@[elab_as_eliminator] def right_moves_nim_rec_on {o : ordinal} {P : (nim o).right_moves → Sort*}
+  (i : (nim o).right_moves) (H : ∀ a < o, P $ to_right_moves_nim ⟨a, H⟩) : P i :=
+by { rw ←to_right_moves_nim.apply_symm_apply i, apply H }
+
 instance is_empty_nim_zero_left_moves : is_empty (nim 0).left_moves :=
 by { rw nim_def, exact ordinal.is_empty_out_zero }