feat(set_theory/game/pgame): golf `le_trans` (#14956)
This also adds `has_le.le.move_left_lf` and `has_le.le.lf_move_right` to enable dot notation. Note that we already have other pgame lemmas in the `has_le.le` namespace like `has_le.le.not_gf`.
To make this dot notation work even when these lemmas are partially-applied, we swap the arguments of `move_left_lf_of_le` and `lf_move_right_of_le`.
