[Merged by Bors] - feat(set_theory/game/pgame): x.move_left i < x and variants

[vihdzp]

---

[semorrison]

Thanks! This is a better way to handle it.

If you feel like adding a few sentences of comments, it might be worth adding cross-references in doc-strings in both directions between move_left_lt and numeric.move_left_le (and similarly for move_right).

I remember finding this point confusing when learning about games, so the pointers to the "missing" lemmas might be helpful for a reader who is confused here.

[semorrison]

bors d+

[bors]

✌️ vihdzp can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[vihdzp]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests