Successors and predecessors of integers #
In this file, we show that ℤ
is both an archimedean SuccOrder
and an archimedean PredOrder
.
Covering relation #
Alias of the reverse direction of Nat.cast_int_covby_iff
.
Mathlib.Data.Int.SuccPred
In this file, we show that ℤ
is both an archimedean SuccOrder
and an archimedean PredOrder
.
Alias of the reverse direction of Nat.cast_int_covby_iff
.