next up previous contents
Next: Propositional Inequality Up: The Natural Numbers Previous: Square Roots

Order relations

An important class of functions on the natural numbers are the order relations, strict less-than and less than or equal. There are many ways to define these relations; the library defines (propositional-valued) $\leq$ as

\begin{displaymath}x \leq y = \exists s {:} \mbox{\it nat}\ x + s = y.

It is hoped that the theorems given in the library are an adequate abstract interface for the relation $\leq$, i.e. any other lemmas are provable from the ones given without using the details of the definition. This can be enforced by using the command Freeze Le.