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.