Commit 2022-02-10 13:11 efa31576

feat(order/conditionally_complete_lattice): cInf_le variant without redundant assumption (#11863) We prove cInf_le' on a conditionally_complete_linear_order_bot. We no longer need the boundedness assumption.