mathlib

1422d387 - feat(order/succ_pred): expand API on `with_bot` and `with_top` (#15016)

feat(order/succ_pred): expand API on `with_bot` and `with_top` (#15016) We add a bunch of `simp` lemmas for successor and predecessors on `with_bot` and `with_top`, and golf some proofs. Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>