Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

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.x:Z
Z.pow_pos x 1 = x
Proof (Z.pow_1_r x).

Lemma Zpower_pos_1_l p : Z.pow_pos 1 p = 1.p:positive
Z.pow_pos 1 p = 1
Proof.p:positive
Z.pow_pos 1 p = 1 now apply (Z.pow_1_l (Zpos p)). Qed.

Lemma Zpower_pos_0_l p : Z.pow_pos 0 p = 0.p:positive
Z.pow_pos 0 p = 0
Proof.p:positive
Z.pow_pos 0 p = 0 now apply (Z.pow_0_l (Zpos p)). Qed.

Lemma Zpower_pos_pos x p : 0 < x -> 0 < Z.pow_pos x p.x:Z
p:positive
0 < x -> 0 < Z.pow_pos x p
Proof.x:Z
p:positive
0 < x -> 0 < Z.pow_pos x p intros.x:Z
p:positive
H:0 < x
0 < Z.pow_pos x p now apply (Z.pow_pos_nonneg x (Zpos p)). Qed.

Notation Zpower_1_r := Z.pow_1_r (only parsing).
Notation Zpower_1_l := Z.pow_1_l (only parsing).
Notation Zpower_0_l := Z.pow_0_l' (only parsing).
Notation Zpower_0_r := Z.pow_0_r (only parsing).
Notation Zpower_2 := Z.pow_2_r (only parsing).
Notation Zpower_gt_0 := Z.pow_pos_nonneg (only parsing).
Notation Zpower_ge_0 := Z.pow_nonneg (only parsing).
Notation Zpower_Zabs := Z.abs_pow (only parsing).
Notation Zpower_Zsucc := Z.pow_succ_r (only parsing).
Notation Zpower_mult := Z.pow_mul_r (only parsing).
Notation Zpower_le_monotone2 := Z.pow_le_mono_r (only parsing).

Theorem Zpower_le_monotone a b c :
 0 < a -> 0 <= b <= c -> a^b <= a^c.a, b, c:Z
0 < a -> 0 <= b <= c -> a ^ b <= a ^ c
Proof.a, b, c:Z
0 < a -> 0 <= b <= c -> a ^ b <= a ^ c intros.a, b, c:Z
H:0 < a
H0:0 <= b <= c
a ^ b <= a ^ c now apply Z.pow_le_mono_r. Qed.

Theorem Zpower_lt_monotone a b c :
 1 < a -> 0 <= b < c -> a^b < a^c.a, b, c:Z
1 < a -> 0 <= b < c -> a ^ b < a ^ c
Proof.a, b, c:Z
1 < a -> 0 <= b < c -> a ^ b < a ^ c intros.a, b, c:Z
H:1 < a
H0:0 <= b < c
a ^ b < a ^ c apply Z.pow_lt_mono_r; auto with zarith. Qed.

Theorem Zpower_gt_1 x y : 1 < x -> 0 < y -> 1 < x^y.x, y:Z
1 < x -> 0 < y -> 1 < x ^ y
Proof.x, y:Z
1 < x -> 0 < y -> 1 < x ^ y apply Z.pow_gt_1. Qed.

Theorem Zmult_power p q r : 0 <= r -> (p*q)^r = p^r * q^r.p, q, r:Z
0 <= r -> (p * q) ^ r = p ^ r * q ^ r
Proof.p, q, r:Z
0 <= r -> (p * q) ^ r = p ^ r * q ^ r intros.p, q, r:Z
H:0 <= r
(p * q) ^ r = p ^ r * q ^ r apply Z.pow_mul_l. Qed.

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.a, b, c:Z
0 <= c -> 0 <= a <= b -> a ^ c <= b ^ c
Proof.a, b, c:Z
0 <= c -> 0 <= a <= b -> a ^ c <= b ^ c intros.a, b, c:Z
H:0 <= c
H0:0 <= a <= b
a ^ c <= b ^ c now apply Z.pow_le_mono_l. Qed.

Lemma Zpower_le_monotone_inv a b c :
  1 < a -> 0 < b -> a^b <= a^c -> b <= c.a, b, c:Z
1 < a -> 0 < b -> a ^ b <= a ^ c -> b <= c
Proof.a, b, c:Z
1 < a -> 0 < b -> a ^ b <= a ^ c -> b <= c
 intros Ha Hb H.a, b, c:Z
Ha:1 < a
Hb:0 < b
H:a ^ b <= a ^ c
b <= c apply (Z.pow_le_mono_r_iff a); trivial.a, b, c:Z
Ha:1 < a
Hb:0 < b
H:a ^ b <= a ^ c
0 <= c
 apply Z.lt_le_incl; apply (Z.pow_gt_1 a); trivial.a, b, c:Z
Ha:1 < a
Hb:0 < b
H:a ^ b <= a ^ c
1 < a ^ c
 apply Z.lt_le_trans with (a^b); trivial.a, b, c:Z
Ha:1 < a
Hb:0 < b
H:a ^ b <= a ^ c
1 < a ^ b now apply Z.pow_gt_1.
Qed.

Notation Zpower_nat_Zpower := Zpower_nat_Zpower (only parsing).

Theorem Zpower2_lt_lin n : 0 <= n -> n < 2^n.n:Z
0 <= n -> n < 2 ^ n
Proof.n:Z
0 <= n -> n < 2 ^ n intros.n:Z
H:0 <= n
n < 2 ^ n now apply Z.pow_gt_lin_r. Qed.

Theorem Zpower2_le_lin n : 0 <= n -> n <= 2^n.n:Z
0 <= n -> n <= 2 ^ n
Proof.n:Z
0 <= n -> n <= 2 ^ n intros.n:Z
H:0 <= n
n <= 2 ^ n apply Z.lt_le_incl.n:Z
H:0 <= n
n < 2 ^ n now apply Z.pow_gt_lin_r. Qed.

Lemma Zpower2_Psize n p :
  Zpos p < 2^(Z.of_nat n) <-> (Pos.size_nat p <= n)%nat.n:nat
p:positive
Z.pos p < 2 ^ Z.of_nat n <-> (Pos.size_nat p <= n)%nat
Proof.n:nat
p:positive
Z.pos p < 2 ^ Z.of_nat n <-> (Pos.size_nat p <= n)%nat
  revert p; induction n.forall p : positive,
Z.pos p < 2 ^ Z.of_nat 0 <-> (Pos.size_nat p <= 0)%nat
n:nat
IHn:forall p : positive, Z.pos p < 2 ^ Z.of_nat n <-> (Pos.size_nat p <= n)%nat
forall p : positive,
Z.pos p < 2 ^ Z.of_nat (S n) <->
(Pos.size_nat p <= S n)%nat
  destruct p; now split.n:nat
IHn:forall p : positive, Z.pos p < 2 ^ Z.of_nat n <-> (Pos.size_nat p <= n)%nat
forall p : positive,
Z.pos p < 2 ^ Z.of_nat (S n) <->
(Pos.size_nat p <= S n)%nat
  assert (Hn := Nat2Z.is_nonneg n).n:nat
IHn:forall p : positive, Z.pos p < 2 ^ Z.of_nat n <-> (Pos.size_nat p <= n)%nat
Hn:0 <= Z.of_nat n
forall p : positive,
Z.pos p < 2 ^ Z.of_nat (S n) <->
(Pos.size_nat p <= S n)%nat
  destruct p; simpl Pos.size_nat.n:nat
IHn:forall p0 : positive,
Z.pos p0 < 2 ^ Z.of_nat n <-> (Pos.size_nat p0 <= n)%nat
Hn:0 <= Z.of_nat n
p:positive
Z.pos p~1 < 2 ^ Z.of_nat (S n) <->
(S (Pos.size_nat p) <= S n)%nat
n:nat
IHn:forall p0 : positive,
Z.pos p0 < 2 ^ Z.of_nat n <-> (Pos.size_nat p0 <= n)%nat
Hn:0 <= Z.of_nat n
p:positive
Z.pos p~0 < 2 ^ Z.of_nat (S n) <->
(S (Pos.size_nat p) <= S n)%nat
n:nat
IHn:forall p : positive, Z.pos p < 2 ^ Z.of_nat n <-> (Pos.size_nat p <= n)%nat
Hn:0 <= Z.of_nat n
1 < 2 ^ Z.of_nat (S n) <-> (1 <= S n)%nat
  -n:nat
IHn:forall p0 : positive,
Z.pos p0 < 2 ^ Z.of_nat n <-> (Pos.size_nat p0 <= n)%nat
Hn:0 <= Z.of_nat n
p:positive
Z.pos p~1 < 2 ^ Z.of_nat (S n) <->
(S (Pos.size_nat p) <= S n)%nat specialize IHn with p.n:nat
p:positive
IHn:Z.pos p < 2 ^ Z.of_nat n <-> (Pos.size_nat p <= n)%nat
Hn:0 <= Z.of_nat n
Z.pos p~1 < 2 ^ Z.of_nat (S n) <->
(S (Pos.size_nat p) <= S n)%nat
    rewrite Pos2Z.inj_xI, Nat2Z.inj_succ, Z.pow_succ_r; omega.
  -n:nat
IHn:forall p0 : positive,
Z.pos p0 < 2 ^ Z.of_nat n <-> (Pos.size_nat p0 <= n)%nat
Hn:0 <= Z.of_nat n
p:positive
Z.pos p~0 < 2 ^ Z.of_nat (S n) <->
(S (Pos.size_nat p) <= S n)%nat specialize IHn with p.n:nat
p:positive
IHn:Z.pos p < 2 ^ Z.of_nat n <-> (Pos.size_nat p <= n)%nat
Hn:0 <= Z.of_nat n
Z.pos p~0 < 2 ^ Z.of_nat (S n) <->
(S (Pos.size_nat p) <= S n)%nat
    rewrite Pos2Z.inj_xO, Nat2Z.inj_succ, Z.pow_succ_r; omega.
  -n:nat
IHn:forall p : positive, Z.pos p < 2 ^ Z.of_nat n <-> (Pos.size_nat p <= n)%nat
Hn:0 <= Z.of_nat n
1 < 2 ^ Z.of_nat (S n) <-> (1 <= S n)%nat split; auto with zarith.n:nat
IHn:forall p : positive, Z.pos p < 2 ^ Z.of_nat n <-> (Pos.size_nat p <= n)%nat
Hn:0 <= Z.of_nat n
(1 <= S n)%nat -> 1 < 2 ^ Z.of_nat (S n)
    intros _.n:nat
IHn:forall p : positive, Z.pos p < 2 ^ Z.of_nat n <-> (Pos.size_nat p <= n)%nat
Hn:0 <= Z.of_nat n
1 < 2 ^ Z.of_nat (S n) apply Z.pow_gt_1.n:nat
IHn:forall p : positive, Z.pos p < 2 ^ Z.of_nat n <-> (Pos.size_nat p <= n)%nat
Hn:0 <= Z.of_nat n
1 < 2
n:nat
IHn:forall p : positive, Z.pos p < 2 ^ Z.of_nat n <-> (Pos.size_nat p <= n)%nat
Hn:0 <= Z.of_nat n
0 < Z.of_nat (S n) easy.n:nat
IHn:forall p : positive, Z.pos p < 2 ^ Z.of_nat n <-> (Pos.size_nat p <= n)%nat
Hn:0 <= Z.of_nat n
0 < Z.of_nat (S n)
    now rewrite Nat2Z.inj_succ, Z.lt_succ_r.
Qed.

Z.pow and modulo

Theorem Zpower_mod p q n :
  0 < n -> (p^q) mod n = ((p mod n)^q) mod n.p, q, n:Z
0 < n -> p ^ q mod n = (p mod n) ^ q mod n
Proof.p, q, n:Z
0 < n -> p ^ q mod n = (p mod n) ^ q mod n
  intros Hn; destruct (Z.le_gt_cases 0 q) as [H1|H1].p, q, n:Z
Hn:0 < n
H1:0 <= q
p ^ q mod n = (p mod n) ^ q mod n
p, q, n:Z
Hn:0 < n
H1:q < 0
p ^ q mod n = (p mod n) ^ q mod n
  -p, q, n:Z
Hn:0 < n
H1:0 <= q
p ^ q mod n = (p mod n) ^ q mod n pattern q; apply natlike_ind; trivial.p, q, n:Z
Hn:0 < n
H1:0 <= q
forall x : Z,
0 <= x ->
p ^ x mod n = (p mod n) ^ x mod n ->
p ^ Z.succ x mod n = (p mod n) ^ Z.succ x mod n
    clear q H1.p, n:Z
Hn:0 < n
forall x : Z,
0 <= x ->
p ^ x mod n = (p mod n) ^ x mod n ->
p ^ Z.succ x mod n = (p mod n) ^ Z.succ x mod n intros q Hq Rec.p, n:Z
Hn:0 < n
q:Z
Hq:0 <= q
Rec:p ^ q mod n = (p mod n) ^ q mod n
p ^ Z.succ q mod n = (p mod n) ^ Z.succ q mod n rewrite !Z.pow_succ_r; trivial.p, n:Z
Hn:0 < n
q:Z
Hq:0 <= q
Rec:p ^ q mod n = (p mod n) ^ q mod n
(p * p ^ q) mod n = (p mod n * (p mod n) ^ q) mod n
    rewrite Z.mul_mod_idemp_l; auto with zarith.p, n:Z
Hn:0 < n
q:Z
Hq:0 <= q
Rec:p ^ q mod n = (p mod n) ^ q mod n
(p * p ^ q) mod n = (p * (p mod n) ^ q) mod n
    rewrite Z.mul_mod, Rec, <- Z.mul_mod; auto with zarith.
  -p, q, n:Z
Hn:0 < n
H1:q < 0
p ^ q mod n = (p mod n) ^ q mod n rewrite !Z.pow_neg_r; auto with zarith.
Qed.

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.a:Z
m:positive
n:Z
n <> 0 -> Zpow_mod_pos a m n = Z.pow_pos a m mod n
Proof.a:Z
m:positive
n:Z
n <> 0 -> Zpow_mod_pos a m n = Z.pow_pos a m mod n
  intros Hn.a:Z
m:positive
n:Z
Hn:n <> 0
Zpow_mod_pos a m n = Z.pow_pos a m mod n induction m.a:Z
m:positive
n:Z
Hn:n <> 0
IHm:Zpow_mod_pos a m n = Z.pow_pos a m mod n
Zpow_mod_pos a m~1 n = Z.pow_pos a m~1 mod n
a:Z
m:positive
n:Z
Hn:n <> 0
IHm:Zpow_mod_pos a m n = Z.pow_pos a m mod n
Zpow_mod_pos a m~0 n = Z.pow_pos a m~0 mod n
a, n:Z
Hn:n <> 0
Zpow_mod_pos a 1 n = Z.pow_pos a 1 mod n
  -a:Z
m:positive
n:Z
Hn:n <> 0
IHm:Zpow_mod_pos a m n = Z.pow_pos a m mod n
Zpow_mod_pos a m~1 n = Z.pow_pos a m~1 mod n rewrite Pos.xI_succ_xO at 2.a:Z
m:positive
n:Z
Hn:n <> 0
IHm:Zpow_mod_pos a m n = Z.pow_pos a m mod n
Zpow_mod_pos a m~1 n =
Z.pow_pos a (Pos.succ m~0) mod n rewrite <- Pos.add_1_r, <- Pos.add_diag.a:Z
m:positive
n:Z
Hn:n <> 0
IHm:Zpow_mod_pos a m n = Z.pow_pos a m mod n
Zpow_mod_pos a m~1 n = Z.pow_pos a (m + m + 1) mod n
    rewrite 2 Zpower_pos_is_exp, Zpower_pos_1_r.a:Z
m:positive
n:Z
Hn:n <> 0
IHm:Zpow_mod_pos a m n = Z.pow_pos a m mod n
Zpow_mod_pos a m~1 n =
(Z.pow_pos a m * Z.pow_pos a m * a) mod n
    rewrite Z.mul_mod, (Z.mul_mod (Z.pow_pos a m)) by trivial.a:Z
m:positive
n:Z
Hn:n <> 0
IHm:Zpow_mod_pos a m n = Z.pow_pos a m mod n
Zpow_mod_pos a m~1 n =
((Z.pow_pos a m mod n * (Z.pow_pos a m mod n)) mod n *
 (a mod n)) mod n
    rewrite <- IHm, <- Z.mul_mod by trivial.a:Z
m:positive
n:Z
Hn:n <> 0
IHm:Zpow_mod_pos a m n = Z.pow_pos a m mod n
Zpow_mod_pos a m~1 n =
(Zpow_mod_pos a m n * Zpow_mod_pos a m n * a) mod n
    simpl.a:Z
m:positive
n:Z
Hn:n <> 0
IHm:Zpow_mod_pos a m n = Z.pow_pos a m mod n
match Zpow_mod_pos a m n with
| 0 => 0
| _ =>
    (Zpow_mod_pos a m n * Zpow_mod_pos a m n * a)
    mod n
end =
(Zpow_mod_pos a m n * Zpow_mod_pos a m n * a) mod n now destruct (Zpow_mod_pos a m n).
  -a:Z
m:positive
n:Z
Hn:n <> 0
IHm:Zpow_mod_pos a m n = Z.pow_pos a m mod n
Zpow_mod_pos a m~0 n = Z.pow_pos a m~0 mod n rewrite <- Pos.add_diag at 2.a:Z
m:positive
n:Z
Hn:n <> 0
IHm:Zpow_mod_pos a m n = Z.pow_pos a m mod n
Zpow_mod_pos a m~0 n = Z.pow_pos a (m + m) mod n
    rewrite Zpower_pos_is_exp.a:Z
m:positive
n:Z
Hn:n <> 0
IHm:Zpow_mod_pos a m n = Z.pow_pos a m mod n
Zpow_mod_pos a m~0 n =
(Z.pow_pos a m * Z.pow_pos a m) mod n
    rewrite Z.mul_mod by trivial.a:Z
m:positive
n:Z
Hn:n <> 0
IHm:Zpow_mod_pos a m n = Z.pow_pos a m mod n
Zpow_mod_pos a m~0 n =
(Z.pow_pos a m mod n * (Z.pow_pos a m mod n)) mod n
    rewrite <- IHm.a:Z
m:positive
n:Z
Hn:n <> 0
IHm:Zpow_mod_pos a m n = Z.pow_pos a m mod n
Zpow_mod_pos a m~0 n =
(Zpow_mod_pos a m n * Zpow_mod_pos a m n) mod n
    simpl.a:Z
m:positive
n:Z
Hn:n <> 0
IHm:Zpow_mod_pos a m n = Z.pow_pos a m mod n
match Zpow_mod_pos a m n with
| 0 => 0
| _ => (Zpow_mod_pos a m n * Zpow_mod_pos a m n) mod n
end = (Zpow_mod_pos a m n * Zpow_mod_pos a m n) mod n now destruct (Zpow_mod_pos a m n).
  -a, n:Z
Hn:n <> 0
Zpow_mod_pos a 1 n = Z.pow_pos a 1 mod n now rewrite Zpower_pos_1_r.
Qed.

Theorem Zpow_mod_correct a m n :
 n <> 0 -> Zpow_mod a m n = (a ^ m) mod n.a, m, n:Z
n <> 0 -> Zpow_mod a m n = a ^ m mod n
Proof.a, m, n:Z
n <> 0 -> Zpow_mod a m n = a ^ m mod n
  intros Hn.a, m, n:Z
Hn:n <> 0
Zpow_mod a m n = a ^ m mod n destruct m; simpl; trivial.a:Z
p:positive
n:Z
Hn:n <> 0
Zpow_mod_pos a p n = Z.pow_pos a p mod n
  -a:Z
p:positive
n:Z
Hn:n <> 0
Zpow_mod_pos a p n = Z.pow_pos a p mod n apply Zpow_mod_pos_correct; auto with zarith.
Qed.

(* Complements about power and number theory. *)

Lemma Zpower_divide p q : 0 < q -> (p | p ^ q).p, q:Z
0 < q -> (p | p ^ q)
Proof.p, q:Z
0 < q -> (p | p ^ q)
  exists (p^(q - 1)).p, q:Z
H:0 < q
p ^ q = p ^ (q - 1) * p
  rewrite Z.mul_comm, <- Z.pow_succ_r; f_equal; auto with zarith.
Qed.

Theorem rel_prime_Zpower_r i p q :
 0 <= i -> rel_prime p q -> rel_prime p (q^i).i, p, q:Z
0 <= i -> rel_prime p q -> rel_prime p (q ^ i)
Proof.i, p, q:Z
0 <= i -> rel_prime p q -> rel_prime p (q ^ i)
  intros Hi Hpq; pattern i; apply natlike_ind; auto with zarith.i, p, q:Z
Hi:0 <= i
Hpq:rel_prime p q
rel_prime p (q ^ 0)
i, p, q:Z
Hi:0 <= i
Hpq:rel_prime p q
forall x : Z,
0 <= x ->
rel_prime p (q ^ x) -> rel_prime p (q ^ Z.succ x)
  simpl.i, p, q:Z
Hi:0 <= i
Hpq:rel_prime p q
rel_prime p 1
i, p, q:Z
Hi:0 <= i
Hpq:rel_prime p q
forall x : Z,
0 <= x ->
rel_prime p (q ^ x) -> rel_prime p (q ^ Z.succ x) apply rel_prime_sym, rel_prime_1.i, p, q:Z
Hi:0 <= i
Hpq:rel_prime p q
forall x : Z,
0 <= x ->
rel_prime p (q ^ x) -> rel_prime p (q ^ Z.succ x)
  clear i Hi.p, q:Z
Hpq:rel_prime p q
forall x : Z,
0 <= x ->
rel_prime p (q ^ x) -> rel_prime p (q ^ Z.succ x) intros i Hi Rec; rewrite Z.pow_succ_r; auto.p, q:Z
Hpq:rel_prime p q
i:Z
Hi:0 <= i
Rec:rel_prime p (q ^ i)
rel_prime p (q * q ^ i)
  apply rel_prime_mult; auto.
Qed.

Theorem rel_prime_Zpower i j p q :
 0 <= i ->  0 <= j -> rel_prime p q -> rel_prime (p^i) (q^j).i, j, p, q:Z
0 <= i ->
0 <= j -> rel_prime p q -> rel_prime (p ^ i) (q ^ j)
Proof.i, j, p, q:Z
0 <= i ->
0 <= j -> rel_prime p q -> rel_prime (p ^ i) (q ^ j)
 intros Hi Hj H.i, j, p, q:Z
Hi:0 <= i
Hj:0 <= j
H:rel_prime p q
rel_prime (p ^ i) (q ^ j) apply rel_prime_Zpower_r; trivial.i, j, p, q:Z
Hi:0 <= i
Hj:0 <= j
H:rel_prime p q
rel_prime (p ^ i) q
 apply rel_prime_sym.i, j, p, q:Z
Hi:0 <= i
Hj:0 <= j
H:rel_prime p q
rel_prime q (p ^ i) apply rel_prime_Zpower_r; trivial.i, j, p, q:Z
Hi:0 <= i
Hj:0 <= j
H:rel_prime p q
rel_prime q p
 now apply rel_prime_sym.
Qed.

Theorem prime_power_prime p q n :
 0 <= n -> prime p -> prime q -> (p | q^n) -> p = q.p, q, n:Z
0 <= n -> prime p -> prime q -> (p | q ^ n) -> p = q
Proof.p, q, n:Z
0 <= n -> prime p -> prime q -> (p | q ^ n) -> p = q
  intros Hn Hp Hq; pattern n; apply natlike_ind; auto; clear n Hn.p, q:Z
Hp:prime p
Hq:prime q
(p | q ^ 0) -> p = q
p, q:Z
Hp:prime p
Hq:prime q
forall x : Z,
0 <= x ->
((p | q ^ x) -> p = q) -> (p | q ^ Z.succ x) -> p = q
  -p, q:Z
Hp:prime p
Hq:prime q
(p | q ^ 0) -> p = q simpl; intros.p, q:Z
Hp:prime p
Hq:prime q
H:(p | 1)
p = q
    assert (2<=p) by (apply prime_ge_2; auto).p, q:Z
Hp:prime p
Hq:prime q
H:(p | 1)
H0:2 <= p
p = q
    assert (p<=1) by (apply Z.divide_pos_le; auto with zarith).p, q:Z
Hp:prime p
Hq:prime q
H:(p | 1)
H0:2 <= p
H1:p <= 1
p = q
    omega.
  -p, q:Z
Hp:prime p
Hq:prime q
forall x : Z,
0 <= x ->
((p | q ^ x) -> p = q) -> (p | q ^ Z.succ x) -> p = q intros n Hn Rec.p, q:Z
Hp:prime p
Hq:prime q
n:Z
Hn:0 <= n
Rec:(p | q ^ n) -> p = q
(p | q ^ Z.succ n) -> p = q
    rewrite Z.pow_succ_r by trivial.p, q:Z
Hp:prime p
Hq:prime q
n:Z
Hn:0 <= n
Rec:(p | q ^ n) -> p = q
(p | q * q ^ n) -> p = q intros.p, q:Z
Hp:prime p
Hq:prime q
n:Z
Hn:0 <= n
Rec:(p | q ^ n) -> p = q
H:(p | q * q ^ n)
p = q
    assert (2<=p) by (apply prime_ge_2; auto).p, q:Z
Hp:prime p
Hq:prime q
n:Z
Hn:0 <= n
Rec:(p | q ^ n) -> p = q
H:(p | q * q ^ n)
H0:2 <= p
p = q
    assert (2<=q) by (apply prime_ge_2; auto).p, q:Z
Hp:prime p
Hq:prime q
n:Z
Hn:0 <= n
Rec:(p | q ^ n) -> p = q
H:(p | q * q ^ n)
H0:2 <= p
H1:2 <= q
p = q
    destruct prime_mult with (2 := H); auto.p, q:Z
Hp:prime p
Hq:prime q
n:Z
Hn:0 <= n
Rec:(p | q ^ n) -> p = q
H:(p | q * q ^ n)
H0:2 <= p
H1:2 <= q
H2:(p | q)
p = q
    apply prime_div_prime; auto.
Qed.

Theorem Zdivide_power_2 x p n :
 0 <= n -> 0 <= x -> prime p -> (x | p^n) -> exists m, x = p^m.x, p, n:Z
0 <= n ->
0 <= x ->
prime p -> (x | p ^ n) -> exists m : Z, x = p ^ m
Proof.x, p, n:Z
0 <= n ->
0 <= x ->
prime p -> (x | p ^ n) -> exists m : Z, x = p ^ m
  intros Hn Hx; revert p n Hn.x:Z
Hx:0 <= x
forall p n : Z,
0 <= n ->
prime p -> (x | p ^ n) -> exists m : Z, x = p ^ m generalize Hx.x:Z
Hx:0 <= x
0 <= x ->
forall p n : Z,
0 <= n ->
prime p -> (x | p ^ n) -> exists m : Z, x = p ^ m
  pattern x; apply Z_lt_induction; auto.x:Z
Hx:0 <= x
forall x0 : Z,
(forall y : Z,
 0 <= y < x0 ->
 0 <= y ->
 forall p n : Z,
 0 <= n ->
 prime p -> (y | p ^ n) -> exists m : Z, y = p ^ m) ->
0 <= x0 ->
forall p n : Z,
0 <= n ->
prime p -> (x0 | p ^ n) -> exists m : Z, x0 = p ^ m
  clear x Hx; intros x IH Hx p n Hn Hp H.x:Z
IH:forall y : Z,
0 <= y < x ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
Hx:0 <= x
p, n:Z
Hn:0 <= n
Hp:prime p
H:(x | p ^ n)
exists m : Z, x = p ^ m
  Z.le_elim Hx; subst.x:Z
IH:forall y : Z,
0 <= y < x ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
Hx:0 < x
p, n:Z
Hn:0 <= n
Hp:prime p
H:(x | p ^ n)
exists m : Z, x = p ^ m
IH:forall y : Z,
0 <= y < 0 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(0 | p ^ n)
exists m : Z, 0 = p ^ m
  apply Z.le_succ_l in Hx; simpl in Hx.x:Z
IH:forall y : Z,
0 <= y < x ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
Hx:1 <= x
p, n:Z
Hn:0 <= n
Hp:prime p
H:(x | p ^ n)
exists m : Z, x = p ^ m
IH:forall y : Z,
0 <= y < 0 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(0 | p ^ n)
exists m : Z, 0 = p ^ m
  Z.le_elim Hx; subst.x:Z
IH:forall y : Z,
0 <= y < x ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
Hx:1 < x
p, n:Z
Hn:0 <= n
Hp:prime p
H:(x | p ^ n)
exists m : Z, x = p ^ m
IH:forall y : Z,
0 <= y < 1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(1 | p ^ n)
exists m : Z, 1 = p ^ m
IH:forall y : Z,
0 <= y < 0 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(0 | p ^ n)
exists m : Z, 0 = p ^ m
  (* x > 1 *)
  case (prime_dec x); intros Hpr.x:Z
IH:forall y : Z,
0 <= y < x ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
Hx:1 < x
p, n:Z
Hn:0 <= n
Hp:prime p
H:(x | p ^ n)
Hpr:prime x
exists m : Z, x = p ^ m
x:Z
IH:forall y : Z,
0 <= y < x ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
Hx:1 < x
p, n:Z
Hn:0 <= n
Hp:prime p
H:(x | p ^ n)
Hpr:~ prime x
exists m : Z, x = p ^ m
IH:forall y : Z,
0 <= y < 1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(1 | p ^ n)
exists m : Z, 1 = p ^ m
IH:forall y : Z,
0 <= y < 0 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(0 | p ^ n)
exists m : Z, 0 = p ^ m
  exists 1; rewrite Z.pow_1_r; apply prime_power_prime with n; auto.x:Z
IH:forall y : Z,
0 <= y < x ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
Hx:1 < x
p, n:Z
Hn:0 <= n
Hp:prime p
H:(x | p ^ n)
Hpr:~ prime x
exists m : Z, x = p ^ m
IH:forall y : Z,
0 <= y < 1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(1 | p ^ n)
exists m : Z, 1 = p ^ m
IH:forall y : Z,
0 <= y < 0 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(0 | p ^ n)
exists m : Z, 0 = p ^ m
  case not_prime_divide with (2 := Hpr); auto.x:Z
IH:forall y : Z,
0 <= y < x ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
Hx:1 < x
p, n:Z
Hn:0 <= n
Hp:prime p
H:(x | p ^ n)
Hpr:~ prime x
forall x0 : Z,
1 < x0 < x /\ (x0 | x) -> exists m : Z, x = p ^ m
IH:forall y : Z,
0 <= y < 1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(1 | p ^ n)
exists m : Z, 1 = p ^ m
IH:forall y : Z,
0 <= y < 0 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(0 | p ^ n)
exists m : Z, 0 = p ^ m
  intros p1 ((Hp1, Hpq1),(q1,->)).p1, q1:Z
Hx:1 < q1 * p1
IH:forall y : Z,
0 <= y < q1 * p1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
Hpr:~ prime (q1 * p1)
H:(q1 * p1 | p ^ n)
Hp1:1 < p1
Hpq1:p1 < q1 * p1
exists m : Z, q1 * p1 = p ^ m
IH:forall y : Z,
0 <= y < 1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(1 | p ^ n)
exists m : Z, 1 = p ^ m
IH:forall y : Z,
0 <= y < 0 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(0 | p ^ n)
exists m : Z, 0 = p ^ m
  assert (Hq1 : 0 < q1) by (apply Z.mul_lt_mono_pos_r with p1; auto with zarith).p1, q1:Z
Hx:1 < q1 * p1
IH:forall y : Z,
0 <= y < q1 * p1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
Hpr:~ prime (q1 * p1)
H:(q1 * p1 | p ^ n)
Hp1:1 < p1
Hpq1:p1 < q1 * p1
Hq1:0 < q1
exists m : Z, q1 * p1 = p ^ m
IH:forall y : Z,
0 <= y < 1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(1 | p ^ n)
exists m : Z, 1 = p ^ m
IH:forall y : Z,
0 <= y < 0 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(0 | p ^ n)
exists m : Z, 0 = p ^ m
  destruct (IH p1) with p n as (r1,Hr1); auto with zarith.p1, q1:Z
Hx:1 < q1 * p1
IH:forall y : Z,
0 <= y < q1 * p1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
Hpr:~ prime (q1 * p1)
H:(q1 * p1 | p ^ n)
Hp1:1 < p1
Hpq1:p1 < q1 * p1
Hq1:0 < q1
(p1 | p ^ n)
p1, q1:Z
Hx:1 < q1 * p1
IH:forall y : Z,
0 <= y < q1 * p1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
Hpr:~ prime (q1 * p1)
H:(q1 * p1 | p ^ n)
Hp1:1 < p1
Hpq1:p1 < q1 * p1
Hq1:0 < q1
r1:Z
Hr1:p1 = p ^ r1
exists m : Z, q1 * p1 = p ^ m
IH:forall y : Z,
0 <= y < 1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(1 | p ^ n)
exists m : Z, 1 = p ^ m
IH:forall y : Z,
0 <= y < 0 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(0 | p ^ n)
exists m : Z, 0 = p ^ m
  transitivity (q1 * p1); trivial.p1, q1:Z
Hx:1 < q1 * p1
IH:forall y : Z,
0 <= y < q1 * p1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
Hpr:~ prime (q1 * p1)
H:(q1 * p1 | p ^ n)
Hp1:1 < p1
Hpq1:p1 < q1 * p1
Hq1:0 < q1
(p1 | q1 * p1)
p1, q1:Z
Hx:1 < q1 * p1
IH:forall y : Z,
0 <= y < q1 * p1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
Hpr:~ prime (q1 * p1)
H:(q1 * p1 | p ^ n)
Hp1:1 < p1
Hpq1:p1 < q1 * p1
Hq1:0 < q1
r1:Z
Hr1:p1 = p ^ r1
exists m : Z, q1 * p1 = p ^ m
IH:forall y : Z,
0 <= y < 1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(1 | p ^ n)
exists m : Z, 1 = p ^ m
IH:forall y : Z,
0 <= y < 0 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(0 | p ^ n)
exists m : Z, 0 = p ^ m exists q1; auto with zarith.p1, q1:Z
Hx:1 < q1 * p1
IH:forall y : Z,
0 <= y < q1 * p1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
Hpr:~ prime (q1 * p1)
H:(q1 * p1 | p ^ n)
Hp1:1 < p1
Hpq1:p1 < q1 * p1
Hq1:0 < q1
r1:Z
Hr1:p1 = p ^ r1
exists m : Z, q1 * p1 = p ^ m
IH:forall y : Z,
0 <= y < 1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(1 | p ^ n)
exists m : Z, 1 = p ^ m
IH:forall y : Z,
0 <= y < 0 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(0 | p ^ n)
exists m : Z, 0 = p ^ m
  destruct (IH q1) with p n as (r2,Hr2); auto with zarith.p1, q1:Z
Hx:1 < q1 * p1
IH:forall y : Z,
0 <= y < q1 * p1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
Hpr:~ prime (q1 * p1)
H:(q1 * p1 | p ^ n)
Hp1:1 < p1
Hpq1:p1 < q1 * p1
Hq1:0 < q1
r1:Z
Hr1:p1 = p ^ r1
0 <= q1 < q1 * p1
p1, q1:Z
Hx:1 < q1 * p1
IH:forall y : Z,
0 <= y < q1 * p1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
Hpr:~ prime (q1 * p1)
H:(q1 * p1 | p ^ n)
Hp1:1 < p1
Hpq1:p1 < q1 * p1
Hq1:0 < q1
r1:Z
Hr1:p1 = p ^ r1
(q1 | p ^ n)
p1, q1:Z
Hx:1 < q1 * p1
IH:forall y : Z,
0 <= y < q1 * p1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
Hpr:~ prime (q1 * p1)
H:(q1 * p1 | p ^ n)
Hp1:1 < p1
Hpq1:p1 < q1 * p1
Hq1:0 < q1
r1:Z
Hr1:p1 = p ^ r1
r2:Z
Hr2:q1 = p ^ r2
exists m : Z, q1 * p1 = p ^ m
IH:forall y : Z,
0 <= y < 1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(1 | p ^ n)
exists m : Z, 1 = p ^ m
IH:forall y : Z,
0 <= y < 0 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(0 | p ^ n)
exists m : Z, 0 = p ^ m
  split; auto with zarith.p1, q1:Z
Hx:1 < q1 * p1
IH:forall y : Z,
0 <= y < q1 * p1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
Hpr:~ prime (q1 * p1)
H:(q1 * p1 | p ^ n)
Hp1:1 < p1
Hpq1:p1 < q1 * p1
Hq1:0 < q1
r1:Z
Hr1:p1 = p ^ r1
q1 < q1 * p1
p1, q1:Z
Hx:1 < q1 * p1
IH:forall y : Z,
0 <= y < q1 * p1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
Hpr:~ prime (q1 * p1)
H:(q1 * p1 | p ^ n)
Hp1:1 < p1
Hpq1:p1 < q1 * p1
Hq1:0 < q1
r1:Z
Hr1:p1 = p ^ r1
(q1 | p ^ n)
p1, q1:Z
Hx:1 < q1 * p1
IH:forall y : Z,
0 <= y < q1 * p1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
Hpr:~ prime (q1 * p1)
H:(q1 * p1 | p ^ n)
Hp1:1 < p1
Hpq1:p1 < q1 * p1
Hq1:0 < q1
r1:Z
Hr1:p1 = p ^ r1
r2:Z
Hr2:q1 = p ^ r2
exists m : Z, q1 * p1 = p ^ m
IH:forall y : Z,
0 <= y < 1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(1 | p ^ n)
exists m : Z, 1 = p ^ m
IH:forall y : Z,
0 <= y < 0 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(0 | p ^ n)
exists m : Z, 0 = p ^ m
  rewrite <- (Z.mul_1_r q1) at 1.p1, q1:Z
Hx:1 < q1 * p1
IH:forall y : Z,
0 <= y < q1 * p1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
Hpr:~ prime (q1 * p1)
H:(q1 * p1 | p ^ n)
Hp1:1 < p1
Hpq1:p1 < q1 * p1
Hq1:0 < q1
r1:Z
Hr1:p1 = p ^ r1
q1 * 1 < q1 * p1
p1, q1:Z
Hx:1 < q1 * p1
IH:forall y : Z,
0 <= y < q1 * p1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
Hpr:~ prime (q1 * p1)
H:(q1 * p1 | p ^ n)
Hp1:1 < p1
Hpq1:p1 < q1 * p1
Hq1:0 < q1
r1:Z
Hr1:p1 = p ^ r1
(q1 | p ^ n)
p1, q1:Z
Hx:1 < q1 * p1
IH:forall y : Z,
0 <= y < q1 * p1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
Hpr:~ prime (q1 * p1)
H:(q1 * p1 | p ^ n)
Hp1:1 < p1
Hpq1:p1 < q1 * p1
Hq1:0 < q1
r1:Z
Hr1:p1 = p ^ r1
r2:Z
Hr2:q1 = p ^ r2
exists m : Z, q1 * p1 = p ^ m
IH:forall y : Z,
0 <= y < 1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(1 | p ^ n)
exists m : Z, 1 = p ^ m
IH:forall y : Z,
0 <= y < 0 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(0 | p ^ n)
exists m : Z, 0 = p ^ m
  apply Z.mul_lt_mono_pos_l; auto with zarith.p1, q1:Z
Hx:1 < q1 * p1
IH:forall y : Z,
0 <= y < q1 * p1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
Hpr:~ prime (q1 * p1)
H:(q1 * p1 | p ^ n)
Hp1:1 < p1
Hpq1:p1 < q1 * p1
Hq1:0 < q1
r1:Z
Hr1:p1 = p ^ r1
(q1 | p ^ n)
p1, q1:Z
Hx:1 < q1 * p1
IH:forall y : Z,
0 <= y < q1 * p1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
Hpr:~ prime (q1 * p1)
H:(q1 * p1 | p ^ n)
Hp1:1 < p1
Hpq1:p1 < q1 * p1
Hq1:0 < q1
r1:Z
Hr1:p1 = p ^ r1
r2:Z
Hr2:q1 = p ^ r2
exists m : Z, q1 * p1 = p ^ m
IH:forall y : Z,
0 <= y < 1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(1 | p ^ n)
exists m : Z, 1 = p ^ m
IH:forall y : Z,
0 <= y < 0 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(0 | p ^ n)
exists m : Z, 0 = p ^ m
  transitivity (q1 * p1); trivial.p1, q1:Z
Hx:1 < q1 * p1
IH:forall y : Z,
0 <= y < q1 * p1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
Hpr:~ prime (q1 * p1)
H:(q1 * p1 | p ^ n)
Hp1:1 < p1
Hpq1:p1 < q1 * p1
Hq1:0 < q1
r1:Z
Hr1:p1 = p ^ r1
(q1 | q1 * p1)
p1, q1:Z
Hx:1 < q1 * p1
IH:forall y : Z,
0 <= y < q1 * p1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
Hpr:~ prime (q1 * p1)
H:(q1 * p1 | p ^ n)
Hp1:1 < p1
Hpq1:p1 < q1 * p1
Hq1:0 < q1
r1:Z
Hr1:p1 = p ^ r1
r2:Z
Hr2:q1 = p ^ r2
exists m : Z, q1 * p1 = p ^ m
IH:forall y : Z,
0 <= y < 1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(1 | p ^ n)
exists m : Z, 1 = p ^ m
IH:forall y : Z,
0 <= y < 0 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(0 | p ^ n)
exists m : Z, 0 = p ^ m exists p1; auto with zarith.p1, q1:Z
Hx:1 < q1 * p1
IH:forall y : Z,
0 <= y < q1 * p1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
Hpr:~ prime (q1 * p1)
H:(q1 * p1 | p ^ n)
Hp1:1 < p1
Hpq1:p1 < q1 * p1
Hq1:0 < q1
r1:Z
Hr1:p1 = p ^ r1
r2:Z
Hr2:q1 = p ^ r2
exists m : Z, q1 * p1 = p ^ m
IH:forall y : Z,
0 <= y < 1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(1 | p ^ n)
exists m : Z, 1 = p ^ m
IH:forall y : Z,
0 <= y < 0 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(0 | p ^ n)
exists m : Z, 0 = p ^ m
  exists (r2 + r1); subst.p, r1, r2:Z
Hx:1 < p ^ r2 * p ^ r1
IH:forall y : Z,
0 <= y < p ^ r2 * p ^ r1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
n:Z
Hn:0 <= n
Hp:prime p
Hpq1:p ^ r1 < p ^ r2 * p ^ r1
Hp1:1 < p ^ r1
Hq1:0 < p ^ r2
Hpr:~ prime (p ^ r2 * p ^ r1)
H:(p ^ r2 * p ^ r1 | p ^ n)
p ^ r2 * p ^ r1 = p ^ (r2 + r1)
IH:forall y : Z,
0 <= y < 1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(1 | p ^ n)
exists m : Z, 1 = p ^ m
IH:forall y : Z,
0 <= y < 0 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(0 | p ^ n)
exists m : Z, 0 = p ^ m
  symmetry.p, r1, r2:Z
Hx:1 < p ^ r2 * p ^ r1
IH:forall y : Z,
0 <= y < p ^ r2 * p ^ r1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
n:Z
Hn:0 <= n
Hp:prime p
Hpq1:p ^ r1 < p ^ r2 * p ^ r1
Hp1:1 < p ^ r1
Hq1:0 < p ^ r2
Hpr:~ prime (p ^ r2 * p ^ r1)
H:(p ^ r2 * p ^ r1 | p ^ n)
p ^ (r2 + r1) = p ^ r2 * p ^ r1
IH:forall y : Z,
0 <= y < 1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(1 | p ^ n)
exists m : Z, 1 = p ^ m
IH:forall y : Z,
0 <= y < 0 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(0 | p ^ n)
exists m : Z, 0 = p ^ m apply Z.pow_add_r.p, r1, r2:Z
Hx:1 < p ^ r2 * p ^ r1
IH:forall y : Z,
0 <= y < p ^ r2 * p ^ r1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
n:Z
Hn:0 <= n
Hp:prime p
Hpq1:p ^ r1 < p ^ r2 * p ^ r1
Hp1:1 < p ^ r1
Hq1:0 < p ^ r2
Hpr:~ prime (p ^ r2 * p ^ r1)
H:(p ^ r2 * p ^ r1 | p ^ n)
0 <= r2
p, r1, r2:Z
Hx:1 < p ^ r2 * p ^ r1
IH:forall y : Z,
0 <= y < p ^ r2 * p ^ r1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
n:Z
Hn:0 <= n
Hp:prime p
Hpq1:p ^ r1 < p ^ r2 * p ^ r1
Hp1:1 < p ^ r1
Hq1:0 < p ^ r2
Hpr:~ prime (p ^ r2 * p ^ r1)
H:(p ^ r2 * p ^ r1 | p ^ n)
0 <= r1
IH:forall y : Z,
0 <= y < 1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(1 | p ^ n)
exists m : Z, 1 = p ^ m
IH:forall y : Z,
0 <= y < 0 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(0 | p ^ n)
exists m : Z, 0 = p ^ m
  generalize Hq1; case r2; now auto with zarith.p, r1, r2:Z
Hx:1 < p ^ r2 * p ^ r1
IH:forall y : Z,
0 <= y < p ^ r2 * p ^ r1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
n:Z
Hn:0 <= n
Hp:prime p
Hpq1:p ^ r1 < p ^ r2 * p ^ r1
Hp1:1 < p ^ r1
Hq1:0 < p ^ r2
Hpr:~ prime (p ^ r2 * p ^ r1)
H:(p ^ r2 * p ^ r1 | p ^ n)
0 <= r1
IH:forall y : Z,
0 <= y < 1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(1 | p ^ n)
exists m : Z, 1 = p ^ m
IH:forall y : Z,
0 <= y < 0 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(0 | p ^ n)
exists m : Z, 0 = p ^ m
  generalize Hp1; case r1; now auto with zarith.IH:forall y : Z,
0 <= y < 1 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(1 | p ^ n)
exists m : Z, 1 = p ^ m
IH:forall y : Z,
0 <= y < 0 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(0 | p ^ n)
exists m : Z, 0 = p ^ m
  (* x = 1 *)
  exists 0; rewrite Z.pow_0_r; auto.IH:forall y : Z,
0 <= y < 0 ->
0 <= y ->
forall p0 n0 : Z,
0 <= n0 ->
prime p0 ->
(y | p0 ^ n0) -> exists m : Z, y = p0 ^ m
p, n:Z
Hn:0 <= n
Hp:prime p
H:(0 | p ^ n)
exists m : Z, 0 = p ^ m
  (* x = 0 *)
  exists n; destruct H; rewrite Z.mul_0_r in H; auto.
Qed.

Z.square: a direct definition of z^2

Notation Psquare_correct := Pos.square_spec (only parsing).
Notation Zsquare_correct := Z.square_spec (only parsing).