Commit 2022-05-22 04:22 a8a211f2

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.