feat(order/succ_pred): define successor orders (#9397)
A successor order is an order in which every (non maximal) element has a least greater element. A predecessor order is an order in which every (non minimal) element has a greatest smaller element. Typical examples are `ℕ`, `ℕ+`, `ℤ`, `fin n`, `ordinal`. Anytime you want to turn `a < b + 1` into `a ≤ b` or `a < b` into `a + 1 ≤ b`, you want a `succ_order`.
