mathlib3

c37ea535 - feat(order/succ_pred): `succ`-Archimedean orders (#9714)

feat(order/succ_pred): `succ`-Archimedean orders (#9714) This defines `succ`-Archimedean orders: orders in which `a ≤ b` means that `succ^[n] a = b` for some `n`.