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)).