Commit 2021-10-19 07:05 1f8c96ba

View on Github →

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 ℕ.

Estimated changes

Created src/data/nat/succ_pred.lean

added theorem nat.pred_iterate

added theorem nat.succ_iterate

Modified src/order/succ_pred.lean

modified theorem succ_order.succ_lt_succ_iff