Successors and predecessors of integers #
In this file, we show that ℤ
is both an archimedean succ_order
and an archimedean pred_order
.
@[protected, instance, reducible]
Equations
- int.succ_order = {succ := int.succ, le_succ := int.succ_order._proof_1, max_of_succ_le := int.succ_order._proof_2, succ_le_of_lt := int.succ_order._proof_3, le_of_lt_succ := int.succ_order._proof_4}
@[protected, instance, reducible]
Equations
- int.pred_order = {pred := int.pred, pred_le := int.pred_order._proof_1, min_of_le_pred := int.pred_order._proof_2, le_pred_of_lt := int.pred_order._proof_3, le_of_pred_lt := int.pred_order._proof_4}
Covering relation #
Alias of the reverse direction of nat.cast_int_covby_iff
.