Commit 2023-01-26 09:45 397a33d9
View on Github →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.