Library Coq.Numbers.Integer.Abstract.ZProperties



Require Export ZAxioms ZMulOrder ZSgnAbs.

This functor summarizes all known facts about Z. For the moment it is only an alias to ZMulOrderPropFunct, which subsumes all others, plus properties of sgn and abs.

Module Type ZPropSig (Z:ZAxiomsExtSig) :=
 ZMulOrderPropFunct Z <+ ZSgnAbsPropSig Z.

Module ZPropFunct (Z:ZAxiomsExtSig) <: ZPropSig Z.
 Include ZPropSig Z.
End ZPropFunct.