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_add`
Mathlib4 pair: https://github.com/leanprover-community/mathlib4/pull/1825
