Library Coq.Numbers.Natural.Abstract.NProperties


Require Export NAxioms.
Require Import NMaxMin NParity NPow NSqrt NLog NDiv NGcd NLcm NBits.

The two following functors summarize all known facts about N.
If necessary, the earlier all-in-one functor NProp could be re-obtained via NBasicProp <+ NExtraProp

Module Type NBasicProp (N:NAxiomsMiniSig) := NMaxMinProp N.

Module Type NExtraProp (N:NAxiomsSig)(P:NBasicProp N) :=
 NParityProp N P <+ NPowProp N P <+ NSqrtProp N P
  <+ NLog2Prop N P <+ NDivProp N P <+ NGcdProp N P <+ NLcmProp N P
  <+ NBitsProp N P.