feat(order/conditionally_complete_lattice): add lemmas (#9237)
* add lemmas about `conditionally_complete_linear_order_bot`; in this
case we can drop some `nonempty` assumptions;
* add lemmas for the case of `[is_well_order α (<)]`; in this case
infimum of a nonempty set is the least element of this set.
