Commit 2022-06-29 23:58 68452ec1

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.