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 (
Zpos 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),
(
m < n)%
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 p x y :
Qpower_positive (
x#y)
p = x ^ Zpos p # (y ^ p).