Commit 2023-01-25 14:10 4d756328
View on Github →feat(order/game_add): add more lemmas (#16082) This PR does the following
- add miscellaneous lemmas on
prod.game_add - add a two-variable recursion principle for
prod.game_addMathlib4 pair: https://github.com/leanprover-community/mathlib4/pull/1825