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.