Successors and predecessors of naturals #

In this file, we show that ℕ is both an archimedean succ_order and an archimedean pred_order.

@[protected, instance]

def nat.succ_order :

Equations

nat.succ_order = {succ := nat.succ, le_succ := nat.succ_order._proof_1, max_of_succ_le := nat.succ_order._proof_2, succ_le_of_lt := nat.succ_order._proof_3, le_of_lt_succ := nat.succ_order._proof_4}

@[protected, instance]

def nat.pred_order :

Equations

nat.pred_order = {pred := nat.pred, pred_le := nat.pred_le, min_of_le_pred := nat.pred_order._proof_1, le_pred_of_lt := nat.pred_order._proof_2, le_of_pred_lt := nat.pred_order._proof_3}

@[simp]

theorem nat.succ_eq_succ :

@[simp]

theorem nat.pred_eq_pred :

theorem nat.succ_iterate (a n : ℕ) :

theorem nat.pred_iterate (a n : ℕ) :

@[protected, instance]

@[protected, instance]