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