mathlib

1f8c96ba - feat(data/nat/succ_pred): `ℕ` is succ- and pred- archimedean (#9730)

feat(data/nat/succ_pred): `ℕ` is succ- and pred- archimedean (#9730) This provides the instances `succ_order ℕ`, `pred_order ℕ`, `is_succ_archimedean ℕ`, `is_pred_archimedean ℕ`.