# mathlibdocumentation

data.int.succ_pred

# Successors and predecessors of integers #

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

@[protected, instance]
Equations
@[protected, instance]
Equations
theorem int.succ_iterate (a : ) (n : ) :
= a + n
theorem int.pred_iterate (a : ) (n : ) :
= a - n
@[protected, instance]
@[protected, instance]