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
.