The directory `lib_nat` is the biggest section of the library so far.
It contains a number of files, each concerning a particular function or set
of functions, so users can load just the theorems relating to the functions
they want. Some files contain only a few theorems in their own right but
load many theorems from other files on which they depend. An example of
this is the file `lib_nat_rels` which loads all the files about
relations on the natural numbers and also most of the files with theorems
about the algebraic structure of nat.

- Natural Numbers: Basic Definitions
- Iteration Principles
- Induction Principles
- Theorems about Successor
- Theorems about Minus
- Theorems about Plus
- Theorems about multiplication
- Square Roots
- Order relations
- The predicate Even
- Max and Min
- Division
- Exponentiation