next up previous contents
Next: Natural Numbers: Basic Definitions Up: The LEGO library - Previous: Inductive Sigma

The Natural Numbers

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.