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