mathlib3

9202b6d1 - feat(order/succ_pred/basic): Intervals and `succ`/`pred` (#13486)