Library Coq.Numbers.NatInt.NZProperties


Require Export NZAxioms NZMulOrder.

This functor summarizes all known facts about NZ. For the moment it is only an alias to NZMulOrderProp, which subsumes all others.

Module Type NZProp := NZMulOrderProp.