Commit 2021-09-30 20:25 64bcb389
View on Github →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.