Library Coq.QArith.Qpower


Require Import Zpow_facts Qfield Qreduction.

Properties of Qpower_positive

Values of Qpower_positive for specific arguments


Lemma Qpower_positive_1 : forall n, Qpower_positive 1 n == 1.

Lemma Qpower_positive_0 : forall n, Qpower_positive 0 n == 0.

Relation of Qpower_positive to zero

Qpower_positive and multiplication, exponent subtraction

Qpower_positive and inversion, division, exponent subtraction

Qpower and exponent multiplication

Qpower_positive decomposition


Lemma Qpower_decomp_positive p x y :
  Qpower_positive (x#y) p = x ^ Zpos p # (y ^ p).

Notation Qpower_decomp := Qpower_decomp_positive (only parsing).

Properties of Qpower

Values of Qpower for specific arguments


Lemma Qpower_0 : forall n, (n<>0)%Z -> 0^n == 0.

Lemma Qpower_1 : forall n, 1^n == 1.

Lemma Qpower_0_r: forall q:Q,
  q^0 == 1.

Lemma Qpower_1_r: forall q:Q,
  q^1 == q.

Relation of Qpower to zero


Lemma Qpower_not_0: forall (a : Q) (z : Z),
  ~ a == 0 -> ~ Qpower a z == 0.

Lemma Qpower_0_le : forall (p : Q) (n : Z), 0 <= p -> 0 <= p^n.

Notation Qpower_pos := Qpower_0_le (only parsing).

Lemma Qpower_0_lt: forall (a : Q) (z : Z), 0 < a -> 0 < Qpower a z.

Relation of Qpower to 1


Lemma Qpower_1_lt_pos:
  forall (q : Q) (n : positive), (1<q)%Q -> (1 < q ^ (Z.pos n))%Q.

Lemma Qpower_1_lt:
  forall (q : Q) (n : Z), (1<q)%Q -> (0<n)%Z -> (1 < q ^ n)%Q.

Lemma Qpower_1_le_pos:
  forall (q : Q) (n : positive), (1<=q)%Q -> (1 <= q ^ (Z.pos n))%Q.

Lemma Qpower_1_le:
  forall (q : Q) (n : Z), (1<=q)%Q -> (0<=n)%Z -> (1 <= q ^ n)%Q.

Qpower and multiplication, exponent addition


Lemma Qmult_power : forall a b n, (a*b)^n == a^n*b^n.

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.

Qpower and inversion, division, exponent subtraction


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_opp : forall a n, a^(-n) == /a^n.

Lemma Qpower_minus: forall (a : Q) (n m : Z),
  ~ a == 0 -> a ^ (n - m) == a ^ n / a ^ m.

Lemma Qpower_minus_pos: forall (a b : positive) (n m : Z),
  (Z.pos a#b) ^ (n - m) == (Z.pos a#b) ^ n * (Z.pos b#a) ^ m.

Lemma Qpower_minus_neg: forall (a b : positive) (n m : Z),
  (Z.neg a#b) ^ (n - m) == (Z.neg a#b) ^ n * (Z.neg b#a) ^ m.

Qpower and exponent multiplication


Lemma Qpower_mult : forall a n m, a^(n*m) == (a^n)^m.

Qpower decomposition


Lemma Qpower_decomp_pos: forall (p : positive) (a : Z) (b : positive),
  (a # b) ^ (Z.pos p) == a ^ (Z.pos p) # (b ^ p)%positive.

Lemma Qpower_decomp_neg_pos: forall (p a b: positive),
  (Z.pos a # b) ^ (Z.neg p) == (Z.pos b) ^ (Z.pos p) # (a ^ p)%positive.

Lemma Qpower_decomp_neg_neg: forall (p a b: positive),
  (Z.neg a # b) ^ (Z.neg p) == (Z.neg b) ^ (Z.pos p) # (a ^ p)%positive.

Compatibility of Qpower with relational operators


Lemma Qpower_lt_compat_l:
  forall (q : Q) (n m : Z), (n < m)%Z -> (1<q)%Q -> (q ^ n < q ^ m)%Q.

Lemma Qpower_le_compat_l:
  forall (q : Q) (n m : Z), (n <= m)%Z -> (1<=q)%Q -> (q ^ n <= q ^ m)%Q.

Lemma Qpower_lt_compat_l_inv:
  forall (q : Q) (n m : Z), (q ^ n < q ^ m)%Q -> (1<q)%Q -> (n < m)%Z.

Lemma Qpower_le_compat_l_inv:
  forall (q : Q) (n m : Z), (q ^ n <= q ^ m)%Q -> (1<q)%Q -> (n <= m)%Z.

Qpower and inject_Z


Lemma Zpower_Qpower : forall (a n:Z), (0<=n)%Z -> inject_Z (a^n) == (inject_Z a)^n.

Square


Lemma Qsqr_nonneg : forall a, 0 <= a^2.

Power of 2 positive upper bound


Lemma Qarchimedean_power2_pos : forall q : Q,
  {p : positive | (q < Z.pos (2^p) # 1)%Q}.