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).

instance Nat.instOrderBot : OrderBot ℕ

Equations

• Nat.instOrderBot = OrderBot.mk Nat.zero_le

instance Nat.instNoMaxOrder : NoMaxOrder ℕ

Equations

• Nat.instNoMaxOrder = ⋯

Miscellaneous lemmas

@[simp]

theorem Nat.bot_eq_zero : ⊥ = 0