Library Coq.Numbers.Natural.Abstract.NProperties
Require
Export
NAxioms
NSub
.
This functor summarizes all known facts about N. For the moment it is only an alias to
NSubPropFunct
, which subsumes all others.
Module
Type
NPropSig
:=
NSubPropFunct
.
Module
NPropFunct
(
N
:
NAxiomsSig
) <:
NPropSig
N
.
Include
NPropSig
N
.
End
NPropFunct
.