Laws about Numbers in Z
Written September 1999.
Last updated September 1999.
|section numlaws parents numdefs, corelaws|
This section contains the CADi version of some laws about
numbers in the mathematical toolkit of Z.
Those laws which depend solely on the definitions in the prelude
are given in the file corelaws.z,
which is a parent of this one.
Theorems about the Natural Numbers
We could here state and prove various useful theorems about ,
both because of their usefulness, and to assist in proving
the consistency of the definitions in numdefs.
The theorems would mainly be to the effect
that is an Abelian monoid under _ * _,
and _ * _ distributes through _ + _.