Library Coq.Numbers.Integer.Abstract.ZProperties


Require Export ZAxioms ZMaxMin ZSgnAbs ZParity ZPow ZDivTrunc ZDivFloor
 ZGcd ZLcm NZLog NZSqrt ZBits.

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

Module Type ZBasicProp (Z:ZAxiomsMiniSig) := ZMaxMinProp Z.

Module Type ZExtraProp (Z:ZAxiomsSig)(P:ZBasicProp Z) :=
 ZSgnAbsProp Z P <+ ZParityProp Z P <+ ZPowProp Z P
 <+ NZSqrtProp Z Z P <+ NZSqrtUpProp Z Z P
 <+ NZLog2Prop Z Z Z P <+ NZLog2UpProp Z Z Z P
 <+ ZDivProp Z P <+ ZQuotProp Z P <+ ZGcdProp Z P <+ ZLcmProp Z P
 <+ ZBitsProp Z P.