mathlib

b1000376 - refactor(order/conditionally_complete_lattice): use `order_bot` (#14568)

refactor(order/conditionally_complete_lattice): use `order_bot` (#14568) Use `order_bot` instead of an explicit `c = ⊥` argument in `well_founded.conditionally_complete_linear_order_with_bot`. Also reuse `linear_order.to_lattice` and add `well_founded.min_le`.