mathlib3

018e9b57 - chore(order/bounded_order): Match the `with_bot` and `with_top` API (#13419)

chore(order/bounded_order): Match the `with_bot` and `with_top` API (#13419) The API for `with_top` and the API for `with_bot` somehow evolved independently from each other, which created frustating disparity in lemmas and argument implicitness. This synchronizes everything (including the layout), generalize a few lemmas from `preorder`/`partial_order` to `has_le`/`has_lt`, and removes the duplicated `is_total (with_bot α) (≤)`/`is_total (with_top α) (≤)` instances.