Library Coq.ZArith.Zpow_facts
Require Import ZArith_base.
Require Import ZArithRing.
Require Import Zcomplements.
Require Export Zpower.
Require Import Zdiv.
Require Import Znumtheory.
Open Local Scope Z_scope.
Lemma Zpower_pos_1_r:
forall x,
Zpower_pos x 1
= x.
Lemma Zpower_pos_1_l:
forall p,
Zpower_pos 1
p = 1.
Lemma Zpower_pos_0_l:
forall p,
Zpower_pos 0
p = 0.
Lemma Zpower_pos_pos:
forall x p,
0
< x -> 0
< Zpower_pos x p.
Theorem Zpower_1_r:
forall z,
z^1
= z.
Theorem Zpower_1_l:
forall z, 0
<= z -> 1
^z = 1.
Theorem Zpower_0_l:
forall z,
z<>0 -> 0
^z = 0.
Theorem Zpower_0_r:
forall z,
z^0
= 1.
Theorem Zpower_2:
forall z,
z^2
= z * z.
Theorem Zpower_gt_0:
forall x y,
0
< x -> 0
<= y -> 0
< x^y.
Theorem Zpower_Zabs:
forall a b,
Zabs (
a^b)
= (Zabs a)^b.
Theorem Zpower_Zsucc:
forall p n, 0
<= n ->
p^(Zsucc n) = p * p^n.
Theorem Zpower_mult:
forall p q r, 0
<= q -> 0
<= r ->
p^(q*r) = (p^q)^r.
Theorem Zpower_le_monotone:
forall a b c,
0
< a -> 0
<= b <= c ->
a^b <= a^c.
Theorem Zpower_lt_monotone:
forall a b c,
1
< a -> 0
<= b < c ->
a^b < a^c.
Theorem Zpower_gt_1 :
forall x y,
1
< x -> 0
< y -> 1
< x^y.
Theorem Zpower_ge_0:
forall x y, 0
<= x -> 0
<= x^y.
Theorem Zpower_le_monotone2:
forall a b c, 0
< a ->
b <= c ->
a^b <= a^c.
Theorem Zmult_power:
forall p q r, 0
<= r ->
(p*q)^r = p^r * q^r.
Hint Resolve Zpower_ge_0 Zpower_gt_0:
zarith.
Theorem Zpower_le_monotone3:
forall a b c,
0
<= c -> 0
<= a <= b ->
a^c <= b^c.
Lemma Zpower_le_monotone_inv:
forall a b c,
1
< a -> 0
< b ->
a^b <= a^c ->
b <= c.
Theorem Zpower_nat_Zpower:
forall p q, 0
<= q ->
p^q = Zpower_nat p (
Zabs_nat q).
Theorem Zpower2_lt_lin:
forall n, 0
<= n ->
n < 2
^n.
Theorem Zpower2_le_lin:
forall n, 0
<= n ->
n <= 2
^n.
Lemma Zpower2_Psize :
forall n p,
Zpos p < 2
^(Z_of_nat n) <-> (
Psize p <= n)%
nat.
A direct way to compute Zpower modulo
Zsquare: a direct definition of z^2