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.
Theorem Zpower_mod:
forall p q n, 0 <
n ->
(
p^q)
mod n = ((
p mod n)^q)
mod n.
A direct way to compute Zpower modulo
Zsquare: a direct definition of z^2