# Library Coq.Numbers.Integer.Abstract.ZPow

Properties of the power function
Require Import Bool ZAxioms ZMulOrder ZParity ZSgnAbs NZPow.
Module Type ZPowProp
(Import A : ZAxiomsSig')
(Import B : ZMulOrderProp A)
(Import C : ZParityProp A B)
(Import D : ZSgnAbsProp A B).
Include NZPowProp A A B.
A particular case of pow_add_r, with no precondition
Lemma pow_twice_r a b : a ^(2* b ) == a ^ b * a ^ b.
Parity of power
Lemma even_pow : forall a b, 0< b -> even (a ^ b) = even a.
Lemma odd_pow : forall a b, 0< b -> odd (a ^ b) = odd a.
Properties of power of negative numbers
Lemma pow_opp_even : forall a b, Even b -> ( - a )^ b == a ^ b.
Lemma pow_opp_odd : forall a b, Odd b -> ( - a )^ b == -( a ^ b ).
Lemma pow_even_abs : forall a b, Even b -> a ^ b == ( abs a )^ b.
Lemma pow_even_nonneg : forall a b, Even b -> 0 <= a ^ b.
Lemma pow_odd_abs_sgn : forall a b, Odd b -> a ^ b == sgn a * ( abs a )^ b.
Lemma pow_odd_sgn : forall a b, 0<= b -> Odd b -> sgn (a ^ b) == sgn a.
Lemma abs_pow : forall a b, abs (a ^ b) == ( abs a )^ b.
End ZPowProp.