(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(**
   pock.
   Pocklington's criterion.
 
   @author Olga Caprotti and Martijn Oostdijk
   @version $Revision$
*)

Require Import Arith.
Require Import ZArith.

Require Import lemmas.
Require Import natZ.
Require Import dec.
Require Import list.
Require Import exp.
Require Import divides.
Require Import prime.
Require Import modulo.
Require Import gcd.
Require Import modprime.
Require Import order.

(**
   For all numbers q in natlist qlist: 1 is a linear combination
   of a^(m*qlist/qi) and n modulo n.
*)

Definition allLinCombMod (a : Z) (n m : nat) (qlist : natlist) :=
  alllist nat
    (fun q : nat =>
     LinCombMod 1 (Exp a (m * multDrop q qlist) - 1) (Z_of_nat n) n) qlist.

Lemma allLinCombMod_ok :
 forall (a : Z) (n m : nat) (qlist : natlist),
 allLinCombMod a n m qlist <->
 (forall qi : nat,
  inlist nat qi qlist ->
  LinCombMod 1 (Exp a (m * multDrop qi qlist) - 1) (Z_of_nat n) n).
Proof.
(* Goal: forall _ : Z.le Z0 n, ZPrime n *)
(* Goal: Z.le Z0 n *)
   intros.
   elim
    (alllist_ok nat
       (fun q : nat =>
        LinCombMod 1 (Exp a (m * multDrop q qlist) - 1) (Z_of_nat n) n) qlist).
(* Goal: forall (_ : forall (_ : alllist nat (fun q : nat => LinCombMod (Zpos xH) (Z.sub (Exp a (Init.Nat.mul m (multDrop q qlist))) (Zpos xH)) (Z.of_nat n) n) qlist) (q : nat) (_ : inlist nat q qlist), LinCombMod (Zpos xH) (Z.sub (Exp a (Init.Nat.mul m (multDrop q qlist))) (Zpos xH)) (Z.of_nat n) n) (_ : forall _ : forall (q : nat) (_ : inlist nat q qlist), LinCombMod (Zpos xH) (Z.sub (Exp a (Init.Nat.mul m (multDrop q qlist))) (Zpos xH)) (Z.of_nat n) n, alllist nat (fun q : nat => LinCombMod (Zpos xH) (Z.sub (Exp a (Init.Nat.mul m (multDrop q qlist))) (Zpos xH)) (Z.of_nat n) n) qlist), iff (allLinCombMod a n m qlist) (forall (qi : nat) (_ : inlist nat qi qlist), LinCombMod (Zpos xH) (Z.sub (Exp a (Init.Nat.mul m (multDrop qi qlist))) (Zpos xH)) (Z.of_nat n) n) *)
   split.
(* Goal: forall _ : Z.le Z0 n, ZPrime n *)
(* Goal: Z.le Z0 n *)
   intros. apply H. assumption. assumption.
(* Goal: forall _ : Z.le Z0 n, ZPrime n *)
(* Goal: Z.le Z0 n *)
   intros. apply H0. assumption.
Qed.

(**
   Pocklington's theorem (finally).
   Proves Pocklington for natural numbers.
 *)

Theorem pocklington :
 forall (n q m : nat) (a : Z) (qlist : natlist),
 n > 1 ->
 n = S (q * m) ->
 q = product qlist ->
 allPrime qlist ->
 Mod (Exp a (pred n)) 1 n ->
 allLinCombMod a n m qlist -> n <= q * q -> Prime n.
Proof.
(* Goal: forall _ : Z.le Z0 n, ZPrime n *)
(* Goal: Z.le Z0 n *)
   intros.
(* Goal: forall _ : Z.le Z0 n, ZPrime n *)
(* Goal: Z.le Z0 n *)
   apply primepropdiv. assumption. intro p. intros.
(* Goal: forall _ : Z.le Z0 n, ZPrime n *)
(* Goal: Z.le Z0 n *)
   elim H6. intros. elim H7. intro pdn. intros.
(* Goal: gt p O *)
(* Goal: Mod a Z0 p *)
(* Goal: gt (Init.Nat.pred n) O *)
(* Goal: Mod (Exp a (Init.Nat.pred n)) (Zpos xH) p *)
(* Goal: Mod (Exp (Exp a m) q) (Zpos xH) p *)
(* Goal: lt (Init.Nat.mul (Init.Nat.pred p) (Init.Nat.pred p)) (Init.Nat.mul p p) *)
   unfold gt in |- *. apply le_lt_trans with (pred p * pred p).
(* Goal: Z.gt n (Zpos xH) *)
   apply le_trans with (q * q). assumption.
(* Goal: forall _ : Z.le Z0 n, ZPrime n *)
(* Goal: Z.le Z0 n *)
   cut (q <= pred p). intros.
(* Goal: Z.gt n (Zpos xH) *)
   apply le_le_mult. assumption. assumption.
(* Goal: Z.gt n (Zpos xH) *)
   apply order_le_predp with (Exp a m). assumption.
(* Goal: forall _ : Z.le Z0 n, ZPrime n *)
(* Goal: Z.le Z0 n *)
   cut (Mod (Exp (Exp a m) q) 1 p). intros.
(* Goal: forall _ : Z.le Z0 n, ZPrime n *)
(* Goal: Z.le Z0 n *)
   elim (order_ex (Exp a m) p). intro r. intros.
(* Goal: forall _ : Z.le Z0 n, ZPrime n *)
(* Goal: Z.le Z0 n *)
   elim H12. intros. elim H14. intros. elim H16. intros.
(* Goal: Order (Exp a m) q p *)
(* Goal: Prime p *)
(* Goal: not (Mod (Exp a m) Z0 p) *)
(* Goal: Mod (Exp (Exp a m) q) (Zpos xH) p *)
(* Goal: lt (Init.Nat.mul (Init.Nat.pred p) (Init.Nat.pred p)) (Init.Nat.mul p p) *)
   elim (le_lt_or_eq r q). intro.
(* Goal: forall _ : Z.le Z0 n, ZPrime n *)
(* Goal: Z.le Z0 n *)
   cut (Divides r q). intros.
(* Goal: forall _ : Z.le Z0 n, ZPrime n *)
(* Goal: Z.le Z0 n *)
   elim (techlemma3 qlist r q). intro qi. intros.
(* Goal: forall _ : Z.le Z0 n, ZPrime n *)
(* Goal: Z.le Z0 n *)
   elim H21. intros. elim H23. intro rdm. intros.
(* Goal: Order (Exp a m) q p *)
(* Goal: lt O r *)
(* Goal: lt r q *)
(* Goal: Divides r q *)
(* Goal: @eq nat q (product qlist) *)
(* Goal: allPrime qlist *)
(* Goal: Divides r q *)
(* Goal: forall _ : @eq nat r q, Order (Exp a m) q p *)
(* Goal: le r q *)
(* Goal: Prime p *)
(* Goal: not (Mod (Exp a m) Z0 p) *)
(* Goal: Mod (Exp (Exp a m) q) (Zpos xH) p *)
(* Goal: lt (Init.Nat.mul (Init.Nat.pred p) (Init.Nat.pred p)) (Init.Nat.mul p p) *)
   elim (allLinCombMod_ok a n m qlist).
(* Goal: forall (_ : forall (_ : allLinCombMod a n m qlist) (qi : nat) (_ : inlist nat qi qlist), LinCombMod (Zpos xH) (Z.sub (Exp a (Init.Nat.mul m (multDrop qi qlist))) (Zpos xH)) (Z.of_nat n) n) (_ : forall _ : forall (qi : nat) (_ : inlist nat qi qlist), LinCombMod (Zpos xH) (Z.sub (Exp a (Init.Nat.mul m (multDrop qi qlist))) (Zpos xH)) (Z.of_nat n) n, allLinCombMod a n m qlist), Order (Exp a m) q p *)
(* Goal: lt O r *)
(* Goal: lt r q *)
(* Goal: Divides r q *)
(* Goal: @eq nat q (product qlist) *)
(* Goal: allPrime qlist *)
(* Goal: Divides r q *)
(* Goal: forall _ : @eq nat r q, Order (Exp a m) q p *)
(* Goal: le r q *)
(* Goal: Prime p *)
(* Goal: not (Mod (Exp a m) Z0 p) *)
(* Goal: Mod (Exp (Exp a m) q) (Zpos xH) p *)
(* Goal: lt (Init.Nat.mul (Init.Nat.pred p) (Init.Nat.pred p)) (Init.Nat.mul p p) *)
   intros AH1 AH2. elim (AH1 H4 qi H22).
(* Goal: forall _ : Z.le Z0 n, ZPrime n *)
(* Goal: Z.le Z0 n *)
   intro alpha. intros. elim H25. intro beta. intros.
(* Goal: Z.gt n (Zpos xH) *)
   elim (mod_0not1 p). assumption.
(* Goal: Mod Z0 (Zpos xH) p *)
(* Goal: lt O r *)
(* Goal: lt r q *)
(* Goal: Divides r q *)
(* Goal: @eq nat q (product qlist) *)
(* Goal: allPrime qlist *)
(* Goal: Divides r q *)
(* Goal: forall _ : @eq nat r q, Order (Exp a m) q p *)
(* Goal: le r q *)
(* Goal: Prime p *)
(* Goal: not (Mod (Exp a m) Z0 p) *)
(* Goal: Mod (Exp (Exp a m) q) (Zpos xH) p *)
(* Goal: lt (Init.Nat.mul (Init.Nat.pred p) (Init.Nat.pred p)) (Init.Nat.mul p p) *)
   apply mod_trans with ((1 - 1) * alpha + Z_of_nat n * beta)%Z.
(* Goal: Mod Z0 (Z.add (Z.mul (Z.sub (Zpos xH) (Zpos xH)) alpha) (Z.mul (Z.of_nat n) beta)) p *)
(* Goal: Mod (Z.add (Z.mul (Z.sub (Zpos xH) (Zpos xH)) alpha) (Z.mul (Z.of_nat n) beta)) (Zpos xH) p *)
(* Goal: lt O r *)
(* Goal: lt r q *)
(* Goal: Divides r q *)
(* Goal: @eq nat q (product qlist) *)
(* Goal: allPrime qlist *)
(* Goal: Divides r q *)
(* Goal: forall _ : @eq nat r q, Order (Exp a m) q p *)
(* Goal: le r q *)
(* Goal: Prime p *)
(* Goal: not (Mod (Exp a m) Z0 p) *)
(* Goal: Mod (Exp (Exp a m) q) (Zpos xH) p *)
(* Goal: lt (Init.Nat.mul (Init.Nat.pred p) (Init.Nat.pred p)) (Init.Nat.mul p p) *)
   rewrite H10. simpl in |- *.
(* Goal: ZLinCombMod (Zpos xH) (Z.sub (ZExp a (Z.of_nat (Init.Nat.mul (Z.abs_nat m) (multDrop q (map Z nat Z.abs_nat qlist))))) (Zpos xH)) n n *)
(* Goal: @eq Z (Z.of_nat (Z.abs_nat m)) m *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.ge m Z0 *)
   rewrite Znat.inj_mult.
(* Goal: Mod Z0 (Z.mul (Z.mul (Z.of_nat p) (Z.of_nat pdn)) beta) p *)
(* Goal: Mod (Z.add (Z.mul (Z.sub (Zpos xH) (Zpos xH)) alpha) (Z.mul (Z.of_nat n) beta)) (Zpos xH) p *)
(* Goal: lt O r *)
(* Goal: lt r q *)
(* Goal: Divides r q *)
(* Goal: @eq nat q (product qlist) *)
(* Goal: allPrime qlist *)
(* Goal: Divides r q *)
(* Goal: forall _ : @eq nat r q, Order (Exp a m) q p *)
(* Goal: le r q *)
(* Goal: Prime p *)
(* Goal: not (Mod (Exp a m) Z0 p) *)
(* Goal: Mod (Exp (Exp a m) q) (Zpos xH) p *)
(* Goal: lt (Init.Nat.mul (Init.Nat.pred p) (Init.Nat.pred p)) (Init.Nat.mul p p) *)
   rewrite Zmult_assoc_reverse.
(* Goal: Mod Z0 (Exp a (Init.Nat.pred n)) p *)
(* Goal: Mod (Exp a (Init.Nat.pred n)) (Zpos xH) p *)
(* Goal: Mod (Exp (Exp a m) q) (Zpos xH) p *)
(* Goal: lt (Init.Nat.mul (Init.Nat.pred p) (Init.Nat.pred p)) (Init.Nat.mul p p) *)
   apply mod_sym.
(* Goal: Mod (Z.mul (Z.of_nat p) (Z.mul (Z.of_nat pdn) beta)) Z0 p *)
(* Goal: Mod (Z.add (Z.mul (Z.sub (Zpos xH) (Zpos xH)) alpha) (Z.mul (Z.of_nat n) beta)) (Zpos xH) p *)
(* Goal: lt O r *)
(* Goal: lt r q *)
(* Goal: Divides r q *)
(* Goal: @eq nat q (product qlist) *)
(* Goal: allPrime qlist *)
(* Goal: Divides r q *)
(* Goal: forall _ : @eq nat r q, Order (Exp a m) q p *)
(* Goal: le r q *)
(* Goal: Prime p *)
(* Goal: not (Mod (Exp a m) Z0 p) *)
(* Goal: Mod (Exp (Exp a m) q) (Zpos xH) p *)
(* Goal: lt (Init.Nat.mul (Init.Nat.pred p) (Init.Nat.pred p)) (Init.Nat.mul p p) *)
   apply mod_nx_0_n.
   apply
    mod_trans
     with ((Exp a (m * multDrop qi qlist) - 1) * alpha + Z_of_nat n * beta)%Z.
(* Goal: Mod (Z.add (Z.mul (Z.sub (Zpos xH) (Zpos xH)) alpha) (Z.mul (Z.of_nat n) beta)) (Z.add (Z.mul (Z.sub (Exp a (Init.Nat.mul m (multDrop qi qlist))) (Zpos xH)) alpha) (Z.mul (Z.of_nat n) beta)) p *)
(* Goal: Mod (Z.add (Z.mul (Z.sub (Exp a (Init.Nat.mul m (multDrop qi qlist))) (Zpos xH)) alpha) (Z.mul (Z.of_nat n) beta)) (Zpos xH) p *)
(* Goal: lt O r *)
(* Goal: lt r q *)
(* Goal: Divides r q *)
(* Goal: @eq nat q (product qlist) *)
(* Goal: allPrime qlist *)
(* Goal: Divides r q *)
(* Goal: forall _ : @eq nat r q, Order (Exp a m) q p *)
(* Goal: le r q *)
(* Goal: Prime p *)
(* Goal: not (Mod (Exp a m) Z0 p) *)
(* Goal: Mod (Exp (Exp a m) q) (Zpos xH) p *)
(* Goal: lt (Init.Nat.mul (Init.Nat.pred p) (Init.Nat.pred p)) (Init.Nat.mul p p) *)
   apply mod_plus_compat. apply mod_mult_compat. apply mod_minus_compat.
(* Goal: Mod (Zpos xH) (Exp a (Init.Nat.mul m (multDrop qi qlist))) p *)
(* Goal: Mod (Zpos xH) (Zpos xH) p *)
(* Goal: Mod alpha alpha p *)
(* Goal: Mod (Z.mul (Z.of_nat n) beta) (Z.mul (Z.of_nat n) beta) p *)
(* Goal: Mod (Z.add (Z.mul (Z.sub (Exp a (Init.Nat.mul m (multDrop qi qlist))) (Zpos xH)) alpha) (Z.mul (Z.of_nat n) beta)) (Zpos xH) p *)
(* Goal: lt O r *)
(* Goal: lt r q *)
(* Goal: Divides r q *)
(* Goal: @eq nat q (product qlist) *)
(* Goal: allPrime qlist *)
(* Goal: Divides r q *)
(* Goal: forall _ : @eq nat r q, Order (Exp a m) q p *)
(* Goal: le r q *)
(* Goal: Prime p *)
(* Goal: not (Mod (Exp a m) Z0 p) *)
(* Goal: Mod (Exp (Exp a m) q) (Zpos xH) p *)
(* Goal: lt (Init.Nat.mul (Init.Nat.pred p) (Init.Nat.pred p)) (Init.Nat.mul p p) *)
   rewrite H24.
(* Goal: Mod (Zpos xH) (Exp a (Init.Nat.mul m (Init.Nat.mul r rdm))) p *)
(* Goal: Mod (Zpos xH) (Zpos xH) p *)
(* Goal: Mod alpha alpha p *)
(* Goal: Mod (Z.mul (Z.of_nat n) beta) (Z.mul (Z.of_nat n) beta) p *)
(* Goal: Mod (Z.add (Z.mul (Z.sub (Exp a (Init.Nat.mul m (multDrop qi qlist))) (Zpos xH)) alpha) (Z.mul (Z.of_nat n) beta)) (Zpos xH) p *)
(* Goal: lt O r *)
(* Goal: lt r q *)
(* Goal: Divides r q *)
(* Goal: @eq nat q (product qlist) *)
(* Goal: allPrime qlist *)
(* Goal: Divides r q *)
(* Goal: forall _ : @eq nat r q, Order (Exp a m) q p *)
(* Goal: le r q *)
(* Goal: Prime p *)
(* Goal: not (Mod (Exp a m) Z0 p) *)
(* Goal: Mod (Exp (Exp a m) q) (Zpos xH) p *)
(* Goal: lt (Init.Nat.mul (Init.Nat.pred p) (Init.Nat.pred p)) (Init.Nat.mul p p) *)
   rewrite mult_assoc.
(* Goal: Mod Z0 (Exp a (Init.Nat.pred n)) p *)
(* Goal: Mod (Exp a (Init.Nat.pred n)) (Zpos xH) p *)
(* Goal: Mod (Exp (Exp a m) q) (Zpos xH) p *)
(* Goal: lt (Init.Nat.mul (Init.Nat.pred p) (Init.Nat.pred p)) (Init.Nat.mul p p) *)
   apply mod_sym.
(* Goal: Mod (Exp a (Nat.mul m q)) (Zpos xH) p *)
(* Goal: Mod (Exp (Exp a m) q) (Zpos xH) p *)
(* Goal: lt (Init.Nat.mul (Init.Nat.pred p) (Init.Nat.pred p)) (Init.Nat.mul p p) *)
   rewrite exp_mult. apply mod_exp1. rewrite exp_mult.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: Mod (ZExp a (Z.sub n (Zpos xH))) (ZExp a (Z.sub n (Zpos xH))) (Z.abs_nat n) *)
(* Goal: Z.ge (Z.sub n (Zpos xH)) Z0 *)
(* Goal: Z.lt Z0 n *)
(* Goal: Mod (ZExp a (Z.sub n (Zpos xH))) (Zpos xH) (Z.abs_nat n) *)
(* Goal: allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map Z nat Z.abs_nat qlist) *)
(* Goal: le (Z.abs_nat n) (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   apply mod_refl. apply mod_refl. apply mod_refl.
(* Goal: Z.gt n (Zpos xH) *)
   apply mod_sym. apply modpq_modp with pdn. rewrite <- H10. assumption.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: Divides r q *)
(* Goal: forall _ : @eq nat r q, Order (Exp a m) q p *)
(* Goal: le r q *)
(* Goal: Prime p *)
(* Goal: not (Mod (Exp a m) Z0 p) *)
(* Goal: Mod (Exp (Exp a m) q) (Zpos xH) p *)
(* Goal: lt (Init.Nat.mul (Init.Nat.pred p) (Init.Nat.pred p)) (Init.Nat.mul p p) *)
   apply (order_div (Exp a m) r p H14 q).
(* Goal: lt O q *)
(* Goal: Mod (Exp (Exp a m) q) (Zpos xH) p *)
(* Goal: forall _ : @eq nat r q, Order (Exp a m) q p *)
(* Goal: le r q *)
(* Goal: Prime p *)
(* Goal: not (Mod (Exp a m) Z0 p) *)
(* Goal: Mod (Exp (Exp a m) q) (Zpos xH) p *)
(* Goal: lt (Init.Nat.mul (Init.Nat.pred p) (Init.Nat.pred p)) (Init.Nat.mul p p) *)
   apply lt_trans with r.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: Z.gt n (Zpos xH) *)
   intro. rewrite <- H19. assumption.
(* Goal: le r q *)
(* Goal: Prime p *)
(* Goal: not (Mod (Exp a m) Z0 p) *)
(* Goal: Mod (Exp (Exp a m) q) (Zpos xH) p *)
(* Goal: lt (Init.Nat.mul (Init.Nat.pred p) (Init.Nat.pred p)) (Init.Nat.mul p p) *)
   apply H18.
(* Goal: lt O q *)
(* Goal: Mod (Exp (Exp a m) q) (Zpos xH) p *)
(* Goal: Prime p *)
(* Goal: not (Mod (Exp a m) Z0 p) *)
(* Goal: Mod (Exp (Exp a m) q) (Zpos xH) p *)
(* Goal: lt (Init.Nat.mul (Init.Nat.pred p) (Init.Nat.pred p)) (Init.Nat.mul p p) *)
   elim (le_lt_or_eq 0 q).
(* Goal: Z.gt n (Zpos xH) *)
   intro. assumption.
(* Goal: Z.gt n (Zpos xH) *)
   intro. rewrite <- H19 in H5. simpl in H5. elim (le_not_lt n 0). assumption.
(* Goal: Z.gt n (Zpos xH) *)
   apply lt_trans with 1. apply lt_O_Sn. assumption. apply le_O_n.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: not (Mod (Exp a m) Z0 p) *)
(* Goal: Mod (Exp (Exp a m) q) (Zpos xH) p *)
(* Goal: lt (Init.Nat.mul (Init.Nat.pred p) (Init.Nat.pred p)) (Init.Nat.mul p p) *)
   apply mod_not_exp_0.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: Z.gt n (Zpos xH) *)
   intro. elim (mod_0not1 p). assumption.
(* Goal: Mod Z0 (Zpos xH) p *)
(* Goal: Mod (Exp (Exp a m) q) (Zpos xH) p *)
(* Goal: lt (Init.Nat.mul (Init.Nat.pred p) (Init.Nat.pred p)) (Init.Nat.mul p p) *)
   apply mod_trans with (Exp a (pred n)).
(* Goal: Mod Z0 (Exp a (Init.Nat.pred n)) p *)
(* Goal: Mod (Exp a (Init.Nat.pred n)) (Zpos xH) p *)
(* Goal: Mod (Exp (Exp a m) q) (Zpos xH) p *)
(* Goal: lt (Init.Nat.mul (Init.Nat.pred p) (Init.Nat.pred p)) (Init.Nat.mul p p) *)
   apply mod_sym.
(* Goal: Mod (Exp a (Init.Nat.pred n)) Z0 p *)
(* Goal: Mod (Exp a (Init.Nat.pred n)) (Zpos xH) p *)
(* Goal: Mod (Exp (Exp a m) q) (Zpos xH) p *)
(* Goal: lt (Init.Nat.mul (Init.Nat.pred p) (Init.Nat.pred p)) (Init.Nat.mul p p) *)
   apply moda0_exp_compat.
(* Goal: gt p O *)
(* Goal: Mod a Z0 p *)
(* Goal: gt (Init.Nat.pred n) O *)
(* Goal: Mod (Exp a (Init.Nat.pred n)) (Zpos xH) p *)
(* Goal: Mod (Exp (Exp a m) q) (Zpos xH) p *)
(* Goal: lt (Init.Nat.mul (Init.Nat.pred p) (Init.Nat.pred p)) (Init.Nat.mul p p) *)
   unfold gt in |- *. apply lt_trans with 1. apply lt_O_Sn.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: Z.gt n (Zpos xH) *)
   apply gt_pred. assumption.
(* Goal: Z.gt n (Zpos xH) *)
   rewrite H0. simpl in |- *. rewrite mult_comm. rewrite exp_mult. assumption.
(* Goal: Mod (Exp (Exp a m) q) (Zpos xH) p *)
(* Goal: lt (Init.Nat.mul (Init.Nat.pred p) (Init.Nat.pred p)) (Init.Nat.mul p p) *)
   rewrite H0 in H3. simpl in H3. rewrite <- H0 in H3.
(* Goal: Mod (Exp (Exp a m) q) (Zpos xH) p *)
(* Goal: lt (Init.Nat.mul (Init.Nat.pred p) (Init.Nat.pred p)) (Init.Nat.mul p p) *)
   apply modpq_modp with pdn.
(* Goal: Z.gt n (Zpos xH) *)
   rewrite <- H10. rewrite <- exp_mult. rewrite mult_comm. assumption.
(* Goal: Z.gt n (Zpos xH) *)
   apply lt_multpred_pp. assumption.
Qed.


(**
   Below is an attempt to restate Pocklington's theorem
   using only numbers from Z. This will make concrete
   computations faster.
 *)

(** ZallLinCombMod is equivalent to AllLinCombMod but uses Z. *)

Definition ZallLinCombMod (a n m N : Z) (qlist : Zlist) :=
  alllist Z
    (fun q : Z => ZLinCombMod 1 (ZExp a (m * zmultDrop q qlist) - 1) n N)
    qlist.

Lemma ZallLinCombMod_ok :
 forall (a n m N : Z) (qlist : Zlist),
 ZallLinCombMod a n m N qlist ->
 forall qi : Z,
 inlist Z qi qlist -> ZLinCombMod 1 (ZExp a (m * zmultDrop qi qlist) - 1) n N.
Proof.
(* Goal: forall _ : Z.le Z0 n, ZPrime n *)
(* Goal: Z.le Z0 n *)
   intros.
   elim
    (alllist_ok Z
       (fun q : Z => ZLinCombMod 1 (ZExp a (m * zmultDrop q qlist) - 1) n N)
       qlist).
(* Goal: forall _ : Z.le Z0 n, ZPrime n *)
(* Goal: Z.le Z0 n *)
   intros. apply H1. assumption. assumption.
Qed.

Lemma alllincombzalllincomb :
 forall (a n m : Z) (qlist : Zlist),
 (0 <= n)%Z ->
 (0 <= m)%Z ->
 allPos qlist ->
 ZallLinCombMod a n m n qlist ->
 allLinCombMod a (Zabs_nat n) (Zabs_nat m) (map _ _ Zabs_nat qlist).
Proof.
(* Goal: forall _ : Z.le Z0 n, ZPrime n *)
(* Goal: Z.le Z0 n *)
   intros.
(* Goal: allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map Z nat Z.abs_nat qlist) *)
   unfold ZallLinCombMod in H.
   elim
    (alllist_ok Z
       (fun q : Z => ZLinCombMod 1 (ZExp a (m * zmultDrop q qlist) - 1) n n)
       qlist).
(* Goal: forall _ : Z.le Z0 n, ZPrime n *)
(* Goal: Z.le Z0 n *)
   intros.
   elim
    (alllist_ok nat
       (fun q0 : nat =>
        LinCombMod 1
          (Exp a (Zabs_nat m * multDrop q0 (map _ _ Zabs_nat qlist)) - 1)
          (Z_of_nat (Zabs_nat n)) (Zabs_nat n)) (map _ _ Zabs_nat qlist)).
(* Goal: forall _ : Z.le Z0 n, ZPrime n *)
(* Goal: Z.le Z0 n *)
   intros.
(* Goal: forall _ : Z.le Z0 n, ZPrime n *)
(* Goal: Z.le Z0 n *)
   apply H6. intros.
(* Goal: Mod (Exp a (Init.Nat.pred (Z.abs_nat n))) (ZExp a (Z.sub n (Zpos xH))) (Z.abs_nat n) *)
(* Goal: Mod (ZExp a (Z.sub n (Zpos xH))) (Zpos xH) (Z.abs_nat n) *)
(* Goal: allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map Z nat Z.abs_nat qlist) *)
(* Goal: le (Z.abs_nat n) (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   rewrite <- inj_zexp.
(* Goal: ZLinCombMod (Zpos xH) (Z.sub (ZExp a (Z.of_nat (Init.Nat.mul (Z.abs_nat m) (multDrop q (map Z nat Z.abs_nat qlist))))) (Zpos xH)) n n *)
(* Goal: @eq Z (Z.of_nat (Z.abs_nat m)) m *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.ge m Z0 *)
   rewrite Znat.inj_mult.
(* Goal: Mod (ZExp a (Z.of_nat (Z.abs_nat (Z.sub n (Zpos xH))))) (ZExp a (Z.sub n (Zpos xH))) (Z.abs_nat n) *)
(* Goal: Z.lt Z0 n *)
(* Goal: Mod (ZExp a (Z.sub n (Zpos xH))) (Zpos xH) (Z.abs_nat n) *)
(* Goal: allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map Z nat Z.abs_nat qlist) *)
(* Goal: le (Z.abs_nat n) (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   rewrite inj_abs_pos.
(* Goal: Mod (ZExp a (Z.of_nat (Z.abs_nat (Z.sub n (Zpos xH))))) (ZExp a (Z.sub n (Zpos xH))) (Z.abs_nat n) *)
(* Goal: Z.lt Z0 n *)
(* Goal: Mod (ZExp a (Z.sub n (Zpos xH))) (Zpos xH) (Z.abs_nat n) *)
(* Goal: allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map Z nat Z.abs_nat qlist) *)
(* Goal: le (Z.abs_nat n) (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   rewrite inj_abs_pos.
(* Goal: LinCombMod (Zpos xH) (Z.sub (ZExp a (Z.mul m (Z.of_nat (multDrop q (map Z nat Z.abs_nat qlist))))) (Zpos xH)) n (Z.abs_nat n) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.ge m Z0 *)
   replace m with (Z_of_nat (Zabs_nat m)).
(* Goal: LinCombMod (Zpos xH) (Z.sub (ZExp a (Z.mul (Z.of_nat (Z.abs_nat m)) (Z.of_nat (multDrop q (map Z nat Z.abs_nat qlist))))) (Zpos xH)) n (Z.abs_nat n) *)
(* Goal: @eq Z (Z.of_nat (Z.abs_nat m)) m *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.ge m Z0 *)
   rewrite <- Znat.inj_mult.
(* Goal: LinCombMod (Zpos xH) (Z.sub (ZExp a (Z.of_nat (Init.Nat.mul (Z.abs_nat m) (multDrop q (map Z nat Z.abs_nat qlist))))) (Zpos xH)) n (Z.abs_nat n) *)
(* Goal: @eq Z (Z.of_nat (Z.abs_nat m)) m *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.ge m Z0 *)
   apply zlincombmodlincombmod.
(* Goal: ZLinCombMod (Zpos xH) (Z.sub (ZExp a (Z.of_nat (Init.Nat.mul (Z.abs_nat m) (multDrop q (map Z nat Z.abs_nat qlist))))) (Zpos xH)) n n *)
(* Goal: @eq Z (Z.of_nat (Z.abs_nat m)) m *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.ge m Z0 *)
   rewrite Znat.inj_mult. rewrite inj_abs_pos.
(* Goal: ZLinCombMod (Zpos xH) (Z.sub (ZExp a (Z.mul m (Z.of_nat (multDrop q (map Z nat Z.abs_nat qlist))))) (Zpos xH)) n n *)
(* Goal: Z.ge m Z0 *)
(* Goal: @eq Z (Z.of_nat (Z.abs_nat m)) m *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.ge m Z0 *)
   rewrite multdropzmultdrop.
(* Goal: ZLinCombMod (Zpos xH) (Z.sub (ZExp a (Z.mul m (zmultDrop (Z.of_nat q) (map nat Z Z.of_nat (map Z nat Z.abs_nat qlist))))) (Zpos xH)) n n *)
(* Goal: Z.ge m Z0 *)
(* Goal: @eq Z (Z.of_nat (Z.abs_nat m)) m *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.ge m Z0 *)
   rewrite inj_abs_pos_list.
(* Goal: ZLinCombMod (Zpos xH) (Z.sub (ZExp a (Z.mul m (zmultDrop (Z.of_nat q) qlist))) (Zpos xH)) n n *)
(* Goal: allPos qlist *)
(* Goal: Z.ge m Z0 *)
(* Goal: @eq Z (Z.of_nat (Z.abs_nat m)) m *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.ge m Z0 *)
   apply H3.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: inlist Z (Z.of_nat q) qlist *)
(* Goal: allPos qlist *)
(* Goal: Z.ge m Z0 *)
(* Goal: @eq Z (Z.of_nat (Z.abs_nat m)) m *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.ge m Z0 *)
   apply inlist_inj_abs_pos_list.
(* Goal: Z.gt n (Zpos xH) *)
   assumption. assumption.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: Z.gt n (Zpos xH) *)
   apply Zle_ge. assumption.
(* Goal: @eq Z (Z.of_nat (Z.abs_nat m)) m *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.ge m Z0 *)
   apply inj_abs_pos.
(* Goal: Z.gt n (Zpos xH) *)
   apply Zle_ge. assumption.
(* Goal: Z.gt n (Zpos xH) *)
   apply Zle_ge. assumption.
(* Goal: Z.gt n (Zpos xH) *)
   apply Zle_ge. assumption.
Qed.

(** Zpocklington is equivalent to pocklington but only uses numbers in Z. *)

Theorem Zpocklington :
 forall (n q m a : Z) (qlist : Zlist),
 (n > 1)%Z ->
 (0 <= q)%Z ->
 (0 <= m)%Z ->
 n = (q * m + 1)%Z ->
 q = zproduct qlist ->
 allZPrime qlist ->
 ZMod (ZExp a (n - 1)) 1 n ->
 ZallLinCombMod a n m n qlist -> (n <= q * q)%Z -> ZPrime n.
Proof.
(* Goal: forall _ : Z.le Z0 n, ZPrime n *)
(* Goal: Z.le Z0 n *)
   intros. cut (0 <= n)%Z. intros.
(* Goal: ZPrime n *)
(* Goal: Z.le Z0 n *)
   rewrite <- (inj_abs_pos n). apply primezprime.
   apply
    (pocklington (Zabs_nat n) (Zabs_nat q) (Zabs_nat m) a
       (map _ _ Zabs_nat qlist)).
(* Goal: Z.gt n (Zpos xH) *)
   change (Zabs_nat n > Zabs_nat 1) in |- *. apply gtzgt. assumption.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
(* Goal: Z.le (Zpos xH) n *)
   unfold Zle in |- *. simpl in |- *. discriminate.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: @eq nat (Z.abs_nat n) (S (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat m))) *)
(* Goal: @eq nat (Z.abs_nat q) (product (map Z nat Z.abs_nat qlist)) *)
(* Goal: allPrime (map Z nat Z.abs_nat qlist) *)
(* Goal: Mod (Exp a (Init.Nat.pred (Z.abs_nat n))) (Zpos xH) (Z.abs_nat n) *)
(* Goal: allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map Z nat Z.abs_nat qlist) *)
(* Goal: le (Z.abs_nat n) (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   rewrite H2. rewrite abs_plus_pos. rewrite abs_mult. rewrite plus_comm.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
(* Goal: Z.le (Zpos xH) n *)
   simpl in |- *. reflexivity.
(* Goal: Z.le Z0 (Z.mul q q) *)
(* Goal: Z.le n (Z.mul q q) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   apply isnat_mult.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
(* Goal: Z.le (Zpos xH) n *)
   unfold Zle in |- *. simpl in |- *. discriminate.
(* Goal: @eq nat (Z.abs_nat q) (product (map Z nat Z.abs_nat qlist)) *)
(* Goal: allPrime (map Z nat Z.abs_nat qlist) *)
(* Goal: Mod (Exp a (Init.Nat.pred (Z.abs_nat n))) (Zpos xH) (Z.abs_nat n) *)
(* Goal: allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map Z nat Z.abs_nat qlist) *)
(* Goal: le (Z.abs_nat n) (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   rewrite H3.
(* Goal: @eq nat (Z.abs_nat (zproduct qlist)) (product (map Z nat Z.abs_nat qlist)) *)
(* Goal: allPrime (map Z nat Z.abs_nat qlist) *)
(* Goal: Mod (Exp a (Init.Nat.pred (Z.abs_nat n))) (Zpos xH) (Z.abs_nat n) *)
(* Goal: allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map Z nat Z.abs_nat qlist) *)
(* Goal: le (Z.abs_nat n) (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   apply zproductproduct.
(* Goal: Z.gt n (Zpos xH) *)
   apply allzprimeallprime. assumption.
(* Goal: Mod (Exp a (Init.Nat.pred (Z.abs_nat n))) (Zpos xH) (Z.abs_nat n) *)
(* Goal: allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map Z nat Z.abs_nat qlist) *)
(* Goal: le (Z.abs_nat n) (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   apply mod_trans with (ZExp a (n - 1)).
(* Goal: Mod (Exp a (Init.Nat.pred (Z.abs_nat n))) (ZExp a (Z.sub n (Zpos xH))) (Z.abs_nat n) *)
(* Goal: Mod (ZExp a (Z.sub n (Zpos xH))) (Zpos xH) (Z.abs_nat n) *)
(* Goal: allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map Z nat Z.abs_nat qlist) *)
(* Goal: le (Z.abs_nat n) (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   rewrite <- inj_zexp.
(* Goal: Mod (ZExp a (Z.of_nat (Init.Nat.pred (Z.abs_nat n)))) (ZExp a (Z.sub n (Zpos xH))) (Z.abs_nat n) *)
(* Goal: Mod (ZExp a (Z.sub n (Zpos xH))) (Zpos xH) (Z.abs_nat n) *)
(* Goal: allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map Z nat Z.abs_nat qlist) *)
(* Goal: le (Z.abs_nat n) (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   rewrite abs_pred_pos.
(* Goal: Mod (ZExp a (Z.of_nat (Z.abs_nat (Z.sub n (Zpos xH))))) (ZExp a (Z.sub n (Zpos xH))) (Z.abs_nat n) *)
(* Goal: Z.lt Z0 n *)
(* Goal: Mod (ZExp a (Z.sub n (Zpos xH))) (Zpos xH) (Z.abs_nat n) *)
(* Goal: allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map Z nat Z.abs_nat qlist) *)
(* Goal: le (Z.abs_nat n) (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   rewrite inj_abs_pos.
(* Goal: Mod (ZExp a (Z.sub n (Zpos xH))) (ZExp a (Z.sub n (Zpos xH))) (Z.abs_nat n) *)
(* Goal: Z.ge (Z.sub n (Zpos xH)) Z0 *)
(* Goal: Z.lt Z0 n *)
(* Goal: Mod (ZExp a (Z.sub n (Zpos xH))) (Zpos xH) (Z.abs_nat n) *)
(* Goal: allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map Z nat Z.abs_nat qlist) *)
(* Goal: le (Z.abs_nat n) (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   apply mod_refl.
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   apply Zle_ge.
(* Goal: Z.le Z0 (Z.sub n (Zpos xH)) *)
(* Goal: Z.lt Z0 n *)
(* Goal: Mod (ZExp a (Z.sub n (Zpos xH))) (Zpos xH) (Z.abs_nat n) *)
(* Goal: allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map Z nat Z.abs_nat qlist) *)
(* Goal: le (Z.abs_nat n) (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   unfold Zminus in |- *.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
(* Goal: Z.le (Zpos xH) n *)
   simpl in |- *.
(* Goal: Z.le Z0 (Z.add n (Zneg xH)) *)
(* Goal: Z.lt Z0 n *)
(* Goal: Mod (ZExp a (Z.sub n (Zpos xH))) (Zpos xH) (Z.abs_nat n) *)
(* Goal: allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map Z nat Z.abs_nat qlist) *)
(* Goal: le (Z.abs_nat n) (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   change (0 <= 0 + n + -1)%Z in |- *.
(* Goal: Z.le Z0 (Z.add (Z.add Z0 n) (Zneg xH)) *)
(* Goal: Z.lt Z0 n *)
(* Goal: Mod (ZExp a (Z.sub n (Zpos xH))) (Zpos xH) (Z.abs_nat n) *)
(* Goal: allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map Z nat Z.abs_nat qlist) *)
(* Goal: le (Z.abs_nat n) (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   rewrite (Zplus_assoc_reverse 0).
(* Goal: Z.le Z0 (Z.add Z0 (Z.add n (Zneg xH))) *)
(* Goal: Z.lt Z0 n *)
(* Goal: Mod (ZExp a (Z.sub n (Zpos xH))) (Zpos xH) (Z.abs_nat n) *)
(* Goal: allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map Z nat Z.abs_nat qlist) *)
(* Goal: le (Z.abs_nat n) (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   rewrite Zplus_comm.
(* Goal: Z.le Z0 (Z.add (Z.add n (Zneg xH)) Z0) *)
(* Goal: Z.lt Z0 n *)
(* Goal: Mod (ZExp a (Z.sub n (Zpos xH))) (Zpos xH) (Z.abs_nat n) *)
(* Goal: allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map Z nat Z.abs_nat qlist) *)
(* Goal: le (Z.abs_nat n) (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   apply (Zlt_left 0 n).
(* Goal: Z.lt Z0 n *)
(* Goal: Mod (ZExp a (Z.sub n (Zpos xH))) (Zpos xH) (Z.abs_nat n) *)
(* Goal: allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map Z nat Z.abs_nat qlist) *)
(* Goal: le (Z.abs_nat n) (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   apply Zlt_trans with 1%Z.
(* Goal: Z.lt Z0 (Zpos xH) *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Mod (ZExp a (Z.sub n (Zpos xH))) (Zpos xH) (Z.abs_nat n) *)
(* Goal: allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map Z nat Z.abs_nat qlist) *)
(* Goal: le (Z.abs_nat n) (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   unfold Zlt in |- *.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
(* Goal: Z.le (Zpos xH) n *)
   simpl in |- *.
(* Goal: @eq comparison Lt Lt *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Mod (ZExp a (Z.sub n (Zpos xH))) (Zpos xH) (Z.abs_nat n) *)
(* Goal: allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map Z nat Z.abs_nat qlist) *)
(* Goal: le (Z.abs_nat n) (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   reflexivity.
(* Goal: Z.lt (Zpos xH) n *)
   apply Zgt_lt.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: Z.lt Z0 n *)
(* Goal: Mod (ZExp a (Z.sub n (Zpos xH))) (Zpos xH) (Z.abs_nat n) *)
(* Goal: allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map Z nat Z.abs_nat qlist) *)
(* Goal: le (Z.abs_nat n) (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   apply Zlt_trans with 1%Z.
(* Goal: Z.lt Z0 (Zpos xH) *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Mod (ZExp a (Z.sub n (Zpos xH))) (Zpos xH) (Z.abs_nat n) *)
(* Goal: allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map Z nat Z.abs_nat qlist) *)
(* Goal: le (Z.abs_nat n) (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   unfold Zlt in |- *.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
(* Goal: Z.le (Zpos xH) n *)
   simpl in |- *.
(* Goal: @eq comparison Lt Lt *)
(* Goal: Z.lt (Zpos xH) n *)
(* Goal: Mod (ZExp a (Z.sub n (Zpos xH))) (Zpos xH) (Z.abs_nat n) *)
(* Goal: allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map Z nat Z.abs_nat qlist) *)
(* Goal: le (Z.abs_nat n) (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   reflexivity.
(* Goal: Z.lt (Zpos xH) n *)
   apply Zgt_lt.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: Mod (ZExp a (Z.sub n (Zpos xH))) (Zpos xH) (Z.abs_nat n) *)
(* Goal: allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map Z nat Z.abs_nat qlist) *)
(* Goal: le (Z.abs_nat n) (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   apply zmodmod.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: allLinCombMod a (Z.abs_nat n) (Z.abs_nat m) (map Z nat Z.abs_nat qlist) *)
(* Goal: le (Z.abs_nat n) (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   apply alllincombzalllincomb.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: allPos qlist *)
(* Goal: ZallLinCombMod a n m n qlist *)
(* Goal: le (Z.abs_nat n) (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   apply allzprimeallpos.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: le (Z.abs_nat n) (Init.Nat.mul (Z.abs_nat q) (Z.abs_nat q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   rewrite <- abs_mult.
(* Goal: le (Z.abs_nat n) (Z.abs_nat (Z.mul q q)) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   apply lezle.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: Z.le Z0 (Z.mul q q) *)
(* Goal: Z.le n (Z.mul q q) *)
(* Goal: Z.ge n Z0 *)
(* Goal: Z.le Z0 n *)
   apply isnat_mult.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: Z.gt n (Zpos xH) *)
   assumption.
(* Goal: Z.gt n (Zpos xH) *)
   apply Zle_ge. assumption.
(* Goal: Z.le Z0 n *)
   apply Zle_trans with 1%Z.
(* Goal: not (@eq comparison (Z.compare Z0 (Zpos xH)) Gt) *)
(* Goal: Z.le (Zpos xH) n *)
   unfold Zle in |- *. simpl in |- *. discriminate.
(* Goal: Z.gt n (Zpos xH) *)
   apply Zlt_le_weak. apply Zgt_lt. assumption.
Qed.
