Successors and predecessors of Fin n
#
In this file, we show that Fin n
is both a SuccOrder
and a PredOrder
. Note that they are
also archimedean, but this is derived from the general instance for well-orderings as opposed
to a specific Fin
instance.
@[simp]