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

It is hoped that the theorems given in the library are an adequate abstract interface for the relation , 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

- Propositional Inequality
- Propositional Strict Inequality
- Propositional Relations
- Boolean-valued Relations
- All order relations