# Library Coq.QArith.Qpower

Require Import Zpow_facts Qfield Qreduction.
Lemma Qpower_positive_1 : forall n, Qpower_positive 1 n == 1.
Lemma Qpower_1 : forall n, 1^ n == 1.
Lemma Qpower_positive_0 : forall n, Qpower_positive 0 n == 0.
Lemma Qpower_0 : forall n, (n <>0)%Z -> 0^ n == 0.
Lemma Qpower_not_0_positive : forall a n, ~ a ==0 -> ~ Qpower_positive a n == 0.
Lemma Qpower_pos_positive : forall p n, 0 <= p -> 0 <= Qpower_positive p n.
Lemma Qpower_pos : forall p n, 0 <= p -> 0 <= p ^ n.
Lemma Qmult_power_positive : forall a b n, Qpower_positive (a * b) n == ( Qpower_positive a n )*( Qpower_positive b n ).
Lemma Qmult_power : forall a b n, ( a * b )^ n == a ^ n * b ^ n.
Lemma Qinv_power_positive : forall a n, Qpower_positive (/ a) n == /( Qpower_positive a n ).
Lemma Qinv_power : forall a n, ( / a )^ n == / a ^ n.
Lemma Qdiv_power : forall a b n, ( a / b )^ n == ( a ^ n / b ^ n ).
Lemma Qinv_power_n : forall n p, (1# p )^ n == / ( inject_Z (' p))^ n.
Lemma Qpower_plus_positive : forall a n m, Qpower_positive a (n + m) == ( Qpower_positive a n )*( Qpower_positive a m ).
Lemma Qpower_opp : forall a n, a ^( - n ) == / a ^ n.
Lemma Qpower_minus_positive : forall a (n m:positive), (Pcompare n m Eq = Gt)%positive -> Qpower_positive a (n - m)%positive == ( Qpower_positive a n )/( Qpower_positive a m ).
Lemma Qpower_plus : forall a n m, ~ a ==0 -> a ^( n + m ) == a ^ n * a ^ m.
Lemma Qpower_plus' : forall a n m, (n + m <> 0)%Z -> a ^( n + m ) == a ^ n * a ^ m.
Lemma Qpower_mult_positive : forall a n m, Qpower_positive a (n * m) == Qpower_positive (Qpower_positive a n) m.
Lemma Qpower_mult : forall a n m, a ^( n * m ) == ( a ^ n )^ m.
Lemma Zpower_Qpower : forall (a n:Z), (0<= n)%Z -> inject_Z (a ^ n) == ( inject_Z a )^ n.
Lemma Qsqr_nonneg : forall a, 0 <= a ^2.
Theorem Qpower_decomp: forall p x y,
Qpower_positive (x # y) p == x ^ Zpos p # ( Z2P (( Zpos y ) ^ Zpos p)).