# The natural numbers form a linear order #

This file contains the linear order instance on the natural numbers.

See note [foundational algebra order theory].

## TODO #

Move the `LinearOrder ℕ` instance here (https://github.com/leanprover-community/mathlib4/pull/13092).

source
instance Nat.instOrderBot :
OrderBot ℕ
Equations

- Nat.instOrderBot = { bot := 0, bot_le := Nat.zero_le }

source
instance Nat.instNoMaxOrder :
NoMaxOrder ℕ

### Miscellaneous lemmas #

source
@[simp]
theorem Nat.bot_eq_zero :
⊥ = 0
source
theorem Nat.isLeast_find {p : ℕ → Prop} [DecidablePred p] (hp : ∃ (n : ℕ), p n) :
IsLeast {n : ℕ | p n} (Nat.find hp)

`Nat.find` is the minimum natural number satisfying a predicate `p`.

source
theorem Set.Nonempty.isLeast_natFind {s : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ s] (hs : s.Nonempty) :
IsLeast s (Nat.find hs)

`Nat.find` is the minimum element of a nonempty set of natural numbers.