[Axiom-developer] Proving Axiom Correct. COQ/Axiom type matching

[Tim Daly]

COQ defines some primitive types. For example, it defines 'nat' which
is the type
of 'natural numbers'.

The corresponding type in Axiom seems to be NonNegativeInteger. At the moment
it seems interesting to try to unify these two types, allowing
primitive Axiom operations
to be expressed in COQ directly.

Unifying base types will allow easier translation of Axiom's algorithms.