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 NZMulOrderPropFunct, which subsumes all others.

Module Type NZPropFunct := NZMulOrderPropSig.