feat(order/lattice): add `left_lt_inf` etc (#14152)
* add `left_lt_sup`, `right_lt_sup`, `left_or_right_lt_sup`, and their `inf` counterparts;
* generalize `is_top_or_exists_gt` and `is_bot_or_exists_lt` to directed orders, replacing `forall_le_or_exists_lt_inf` and `forall_le_or_exists_lt_sup`;
* generalize `exists_lt_of_sup` and `exists_lt_of_inf` to directed orders, rename them to `exists_lt_of_directed_le` and `exists_lt_of_directed_ge`.
