Library Coq.Numbers.Integer.Abstract.ZProperties

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

This functor summarizes all known facts about Z.

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