`Nat.Upto`

#

`Nat.Upto p`

, with `p`

a predicate on `ℕ`

, is a subtype of elements `n : ℕ`

such that no value
(strictly) below `n`

satisfies `p`

.

This type has the property that `>`

is well-founded when `∃ i, p i∃ i, p i`

, which allows us to implement
searches on `ℕ`

, starting at `0`

and with an unknown upper-bound.

It is similar to the well founded relation constructed to define `Nat.find`

with
the difference that, in `Nat.Upto p`

, `p`

does not need to be decidable. In fact,
`Nat.find`

could be slightly altered to factor decidability out of its
well founded relation and would then fulfill the same purpose as this file.

The subtype of natural numbers `i`

which have the property that
no `j`

less than `i`

satisfies `p`

. This is an initial segment of the
natural numbers, up to and including the first value satisfying `p`

.

We will be particularly interested in the case where there exists a value
satisfying `p`

, because in this case the `>`

relation is well-founded.

The "greater than" relation on `Upto p`

is well founded if (and only if) there exists a value
satisfying `p`

.