# Library Coq.ZArith.Zpow_facts

Require Import ZArith_base ZArithRing Zcomplements Zdiv Znumtheory.
Require Export Zpower.
Local Open Scope Z_scope.
Properties of the power function over Z
Nota: the usual properties of Z.pow are now already provided by BinInt.Z. Only remain here some compatibility elements, as well as more specific results about power and modulo and/or primality.
Lemma Zpower_pos_1_r x : Z.pow_pos x 1 = x.
Lemma Zpower_pos_1_l p : Z.pow_pos 1 p = 1.
Lemma Zpower_pos_0_l p : Z.pow_pos 0 p = 0.
Lemma Zpower_pos_pos x p : 0 < x -> 0 < Z.pow_pos x p.
Notation Zpower_1_r := Z.pow_1_r (compat "8.3").
Notation Zpower_1_l := Z.pow_1_l (compat "8.3").
Notation Zpower_0_l := Z.pow_0_l' (compat "8.3").
Notation Zpower_0_r := Z.pow_0_r (compat "8.3").
Notation Zpower_2 := Z.pow_2_r (compat "8.3").
Notation Zpower_gt_0 := Z.pow_pos_nonneg (compat "8.3").
Notation Zpower_ge_0 := Z.pow_nonneg (compat "8.3").
Notation Zpower_Zabs := Z.abs_pow (compat "8.3").
Notation Zpower_Zsucc := Z.pow_succ_r (compat "8.3").
Notation Zpower_mult := Z.pow_mul_r (compat "8.3").
Notation Zpower_le_monotone2 := Z.pow_le_mono_r (compat "8.3").
Theorem Zpower_le_monotone a b c :
0 < a -> 0 <= b <= c -> a ^ b <= a ^ c.
Theorem Zpower_lt_monotone a b c :
1 < a -> 0 <= b < c -> a ^ b < a ^ c.
Theorem Zpower_gt_1 x y : 1 < x -> 0 < y -> 1 < x ^ y.
Theorem Zmult_power p q r : 0 <= r -> ( p * q )^ r = p ^ r * q ^ r.
Hint Resolve Z.pow_nonneg Z.pow_pos_nonneg : zarith.
Theorem Zpower_le_monotone3 a b c :
0 <= c -> 0 <= a <= b -> a ^ c <= b ^ c.
Lemma Zpower_le_monotone_inv a b c :
1 < a -> 0 < b -> a ^ b <= a ^ c -> b <= c.
Notation Zpower_nat_Zpower := Zpower_nat_Zpower (only parsing).
Theorem Zpower2_lt_lin n : 0 <= n -> n < 2^ n.
Theorem Zpower2_le_lin n : 0 <= n -> n <= 2^ n.
Lemma Zpower2_Psize n p :
Zpos p < 2^( Z.of_nat n ) <-> (Pos.size_nat p <= n)%nat.

# Z.pow and modulo

Theorem Zpower_mod p q n :
0 < n -> ( p ^ q ) mod n = ( ( p mod n )^ q ) mod n.
A direct way to compute Z.pow 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 mod n
| Zpos p => Zpow_mod_pos a p n
| Zneg p => 0
end.
Theorem Zpow_mod_pos_correct a m n :
n <> 0 -> Zpow_mod_pos a m n = ( Z.pow_pos a m ) mod n.
Theorem Zpow_mod_correct a m n :
n <> 0 -> Zpow_mod a m n = ( a ^ m ) mod n.
Lemma Zpower_divide p q : 0 < q -> ( p | p ^ q ).
Theorem rel_prime_Zpower_r i p q :
0 <= i -> rel_prime p q -> rel_prime p (q ^ i).
Theorem rel_prime_Zpower i j p q :
0 <= i -> 0 <= j -> rel_prime p q -> rel_prime (p ^ i) (q ^ j).
Theorem prime_power_prime p q n :
0 <= n -> prime p -> prime q -> ( p | q ^ n ) -> p = q.
Theorem Zdivide_power_2 x p n :
0 <= n -> 0 <= x -> prime p -> ( x | p ^ n ) -> exists m , x = p ^ m.

# Z.square: a direct definition of z^2

Notation Psquare := Pos.square (compat "8.3").
Notation Zsquare := Z.square (compat "8.3").
Notation Psquare_correct := Pos.square_spec (compat "8.3").
Notation Zsquare_correct := Z.square_spec (compat "8.3").