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
.