The natural numbers as a linearly ordered commutative semiring #
We also have a variety of lemmas which have been deferred from
Data.Nat.Basic because it is
easier to prove them with this ordered semiring instance available.
You may find that some theorems can be moved back to
Data.Nat.Basic by modifying their proofs.
Extra instances to short-circuit type class resolution and ensure computability
Equalities and inequalities involving zero and one #
Recursion and induction principles #
This section is here due to dependencies -- the lemmas here require some of the lemmas proved above, and some of the results in later sections depend on the definitions in this section.
Given a predicate on two naturals
P : ℕ → ℕ → Prop,
P a b is true for all
a < b if
P (a + 1) (a + 1) is true for all
P 0 (b + 1) is true for all
b and for all
a < b,
P (a + 1) b is true and
P a (b + 1) is true implies
P (a + 1) (b + 1) is true.