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.