Library Coq.Numbers.NatInt.NZAxioms
Initial Author : Evgeny Makarov, INRIA, 2007
Axiomatization of a domain with zero, successor, predecessor,
and a bi-directional induction principle. We require P (S n) = n
but not the other way around, since this domain is meant
to be either N or Z. In fact it can be a few other things,
for instance Z/nZ (See file NZDomain for a study of that).
Axiomatization of basic operations : + - *
Old name for the same interface:
Axiomatization of order
NB: the compatibility of le can be proved later from lt_wd
and lt_eq_cases
Everything together :
Same, plus a comparison function.