Successors and predecessors of naturals #
In this file, we show that ℕ
is both an archimedean succOrder
and an archimedean predOrder
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Covering relation #
Alias of the reverse direction of Fin.coe_covby_iff
.