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 Int.natCast_covBy
.
In this file, we show that ℤ
is both an archimedean SuccOrder
and an archimedean PredOrder
.
Alias of the reverse direction of Int.natCast_covBy
.