mathlib3

feat(order/succ_pred/limit): predecessor from a `succ_order`

#15614

Open