Commit 2024-09-06 22:51 5695a9fb

feat(Algebra/Order/SuccPred): typeclass for succ x = x + 1 (#16484) We create the SuccAddOrder typeclass for SuccOrders satisfying succ x = x + 1. The instances of this are ℕ, ℤ, ℕ∞, and Ordinal (as well as the type alias NatOrdinal). On such types, x + 1 should be the preferred form to write succ x. This typeclass avoids the need of having to rewrite x + 1 as succ x and back just to apply the common lemmas on SuccOrder. Moreover, there's been talk on Zulip about generalizing Order.succ and Order.pred to arbitrary preorders. This would make it so that we could no longer set the def-eq succ x = x + 1, but having this typeclass means that's not really an issue. We dually define the PredSubOrder typeclass for pred x = x - 1. This one is admittedly quite more niche, with the only instances being ℕ and ℤ.