mathlib

397a33d9 - chore(set_theory/game/nim): golf `grundy_value_nim_add_nim` (#15878)

chore(set_theory/game/nim): golf `grundy_value_nim_add_nim` (#15878) We also remove `exists_ordinal_move_left_eq` and `exists_move_left_eq`, as they just express in a roundabout way that `to_left_moves_nim` is an equivalence.