mathlib3

cf917732 - refactor(*): split `order_{top,bot}` from `lattice` hierarchy (#9891)

refactor(*): split `order_{top,bot}` from `lattice` hierarchy (#9891) Rename `bounded_lattice` to `bounded_order`. Split out `order_{top,bot}` and `bounded_order` from the order hierarchy. That means that we no longer have `semilattice_{sup,inf}_{top,bot}`, but use the `[order_top]` as a mixin to `semilattice_inf`, for example. Similarly, `lattice` and `bounded_order` instead of what was before `bounded_lattice`. Similarly, `distrib_lattice` and `bounded_order` instead of what was before `bounded_distrib_lattice`.