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

# Zpower and modulo

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
Fixpoint Zpow_mod_pos (a: Z)(m: positive)(n : Z) : Z :=
match m with
| xH => a mod n
| xO m' =>
let z := Zpow_mod_pos a m' n in
match z with
| 0 => 0
| _ => (z * z) mod n
end
| xI m' =>
let z := Zpow_mod_pos a m' n in
match z with
| 0 => 0
| _ => (z * z * a) mod n
end
end.
Definition Zpow_mod a m n :=
match m with
| 0 => 1
| Zpos p => Zpow_mod_pos a p n
| Zneg p => 0
end.
Theorem Zpow_mod_pos_correct: forall a m n, 0 < n ->
Zpow_mod_pos a m n = (Zpower_pos a m) mod n.
Theorem Zpow_mod_correct: forall a m n, 1 < n -> 0 <= m ->
Zpow_mod a m n = (a ^ m) mod n.
Lemma Zpower_divide: forall p q, 0 < q -> (p | p ^ q).
Theorem rel_prime_Zpower_r: forall i p q, 0 < i ->
rel_prime p q -> rel_prime p (q^i).
Theorem rel_prime_Zpower: forall i j p q, 0 <= i -> 0 <= j ->
rel_prime p q -> rel_prime (p^i) (q^j).
Theorem prime_power_prime: forall p q n, 0 <= n ->
prime p -> prime q -> (p | q^n) -> p = q.
Theorem Zdivide_power_2: forall x p n, 0 <= n -> 0 <= x -> prime p ->
(x | p^n) -> exists m, x = p^m.

# Zsquare: a direct definition of z^2

Fixpoint Psquare (p: positive): positive :=
match p with
| xH => xH
| xO p => xO (xO (Psquare p))
| xI p => xI (xO (Pplus (Psquare p) p))
end.
Definition Zsquare p :=
match p with
| Z0 => Z0
| Zpos p => Zpos (Psquare p)
| Zneg p => Zpos (Psquare p)
end.
Theorem Psquare_correct: forall p, Psquare p = (p * p)%positive.
Theorem Zsquare_correct: forall p, Zsquare p = p * p.