(* 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                                                     *)


(**
   fermat.
   Fermat's little theorem.
   
   @author 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 modprime.

(** * No double elements modulo p. *)

Definition nodoubles (p : nat) (l : Zlist) : Prop :=
  forall x : Z,
  inlist Z x l -> forall y : Z, inlist Z y (zdrop x l) -> ~ Mod x y p.

Lemma nodoubles_nil : forall p : nat, nodoubles p (Nil Z).
Proof.
(* Goal: nodoubles p (Cons Z h t) *)
   unfold nodoubles in |- *. simpl in |- *. intros. elim H0.
Qed.

Lemma nodoubles_drop :
 forall (p : nat) (l : Zlist) (x : Z),
 nodoubles p l -> nodoubles p (zdrop x l).
Proof.
(* Goal: nodoubles p (Cons Z h t) *)
   unfold nodoubles in |- *. intros. apply H.
(* Goal: inlist Z z l *)
(* Goal: Mod x y p *)
(* Goal: inlist Z x (zdrop z l) *)
(* Goal: inlist Z y (zdrop z l) *)
   apply zdrop_inlist_weak with x. assumption.
(* Goal: inlist Z z l *)
(* Goal: Mod x y p *)
(* Goal: inlist Z x (zdrop z l) *)
(* Goal: inlist Z y (zdrop z l) *)
   apply zdrop_inlist_weak with x. rewrite zdrop_swap. assumption.
Qed.

Lemma nodoubles_ind :
 forall (p : nat) (h : Z) (t : Zlist),
 (forall x : Z, inlist Z x t -> ~ Mod h x p) ->
 nodoubles p t -> nodoubles p (Cons Z h t).
Proof.
(* Goal: nodoubles p (Cons Z h t) *)
   intros. unfold nodoubles in |- *. intros.
(* Goal: not (Mod x y p) *)
   elim (zeqdec x h).
(* Goal: not (@eq Z z y) *)
(* Goal: inlist Z z l *)
(* Goal: and (Mod z z p) (permmod p (zdrop z (zdrop x l)) (zdrop z (zdrop y l))) *)
   intro. rewrite zdrop_head_eq in H2.
(* Goal: not (Mod a Z0 p) *)
   rewrite H3. apply (H y). assumption. assumption.
(* Goal: not (@eq Z z y) *)
(* Goal: inlist Z z l *)
(* Goal: and (Mod z z p) (permmod p (zdrop z (zdrop x l)) (zdrop z (zdrop y l))) *)
   intro. rewrite zdrop_head_neq in H2.
(* Goal: not (Mod x y p) *)
(* Goal: not (@eq Z x h) *)
   elim (zeqdec y h).
(* Goal: not (@eq Z z y) *)
(* Goal: inlist Z z l *)
(* Goal: and (Mod z z p) (permmod p (zdrop z (zdrop x l)) (zdrop z (zdrop y l))) *)
   intro. rewrite H4. intro. elim (H x).
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   elim (inlist_head_neq Z x h t). intros.
(* Goal: not (Mod a Z0 p) *)
   apply H6. assumption. assumption.
(* Goal: not (Mod a Z0 p) *)
   apply mod_sym. assumption.
(* Goal: not (@eq Z z y) *)
(* Goal: inlist Z z l *)
(* Goal: and (Mod z z p) (permmod p (zdrop z (zdrop x l)) (zdrop z (zdrop y l))) *)
   intro. unfold nodoubles in H0.
(* Goal: not (Mod x y p) *)
(* Goal: not (@eq Z x h) *)
   apply (H0 x).
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   elim (inlist_head_neq Z x h t). intros.
(* Goal: not (Mod a Z0 p) *)
   apply H5. assumption. assumption.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   elim (inlist_head_neq Z y h (zdrop x t)). intros.
(* Goal: not (Mod a Z0 p) *)
   apply H5. assumption. assumption.
(* Goal: not (Mod a Z0 p) *)
   assumption.
Qed.

(** * All elements from l1 occur in l2 modulo p. *)

Definition allex (p : nat) (l0 l1 : Zlist) : Prop :=
  forall x : Z, inlist Z x l0 -> exists y : Z, inlist Z y l1 /\ Mod x y p.

Lemma allex_nodoubles_drop :
 forall (p : nat) (l0 l1 : Zlist) (x0 x1 : Z),
 Prime p ->
 Mod x0 x1 p ->
 inlist Z x0 l0 ->
 inlist Z x1 l1 ->
 nodoubles p l0 -> allex p l0 l1 -> allex p (zdrop x0 l0) (zdrop x1 l1).
Proof.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros.
(* Goal: allex p (until (Init.Nat.pred p)) (mapmult a (until (Init.Nat.pred p))) *)
   unfold allex in |- *. intros x Hx.
(* Goal: @ex Z (fun y : Z => and (inlist Z y (zdrop x1 l1)) (Mod x y p)) *)
   elim (H4 x). intros y Hy.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   elim Hy. intros.
(* Goal: @ex Z (fun x1 : Z => and (inlist Z x1 l1) (and (Mod x x1 p) (permmod p (zdrop x l0) (zdrop x1 l1)))) *)
(* Goal: inlist Z x l0 *)
   split with y.
(* Goal: and (Mod x y p) (permmod p (zdrop x l0) (zdrop y l1)) *)
(* Goal: inlist Z x l0 *)
   split. apply zdrop_neq_inlist.
(* Goal: not (@eq Z z y) *)
(* Goal: inlist Z z l *)
(* Goal: and (Mod z z p) (permmod p (zdrop z (zdrop x l)) (zdrop z (zdrop y l))) *)
   intro. rewrite H7 in H6.
(* Goal: False *)
(* Goal: inlist Z y l1 *)
(* Goal: Mod x y p *)
(* Goal: inlist Z x l0 *)
   elim H3 with x x0.
(* Goal: not (Mod a Z0 p) *)
   apply zdrop_inlist_weak with x0. assumption.
(* Goal: not (Mod a Z0 p) *)
   apply zdrop_inlist_swap. assumption. assumption.
(* Goal: not (Mod a Z0 p) *)
   apply mod_trans with x1. assumption.
(* Goal: not (Mod a Z0 p) *)
   apply mod_sym. assumption.
(* Goal: not (Mod a Z0 p) *)
   assumption. assumption.
(* Goal: not (Mod a Z0 p) *)
   apply zdrop_inlist_weak with x0. assumption.
Qed.

(** * The list of integers between 1 and n (inclusive) *)

Fixpoint until (n : nat) : Zlist :=
  match n with
  | O => Nil Z
  | S n => Cons Z (Z_of_nat (S n)) (until n)
  end.

Lemma until_ok :
 forall (n : nat) (x : Z), (0 < x <= Z_of_nat n)%Z -> inlist Z x (until n).
Proof.
(* Goal: forall (n p : nat) (l0 l1 : Zlist) (_ : @eq nat n (length Z l0)) (_ : @eq nat n (length Z l1)) (_ : Prime p) (_ : @eq nat (length Z l0) (length Z l1)) (_ : nodoubles p l0) (_ : allex p l0 l1), permmod p l0 l1 *)
   simple induction n.
(* Goal: permmod p (zdrop x (Nil Z)) (zdrop y (Nil Z)) *)
(* Goal: @eq nat (length Z l) O *)
(* Goal: forall (n : nat) (_ : forall (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat n (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l)) (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat (S n) (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l) *)
   simpl in |- *. intros. elim H. intros.
(* Goal: not (Mod a Z0 p) *)
   elim (Zle_not_lt x 0). assumption. assumption.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros m IH. intros. elim H. intros.
(* Goal: inlist Z x (until (S m)) *)
   elim (Zle_lt_or_eq x (Z_of_nat (S m))).
(* Goal: permmod p (zdrop x (Nil Z)) (zdrop y (Nil Z)) *)
(* Goal: @eq nat (length Z l) O *)
(* Goal: forall (n : nat) (_ : forall (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat n (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l)) (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat (S n) (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l) *)
   intros. unfold inlist in |- *. simpl in |- *. right. unfold inlist in IH.
(* Goal: not (Mod a Z0 p) *)
   apply IH. split. assumption.
(* Goal: not (Mod a Z0 p) *)
   apply Zlt_succ_le. rewrite <- Znat.inj_S. assumption.
(* Goal: not (@eq Z z y) *)
(* Goal: inlist Z z l *)
(* Goal: and (Mod z z p) (permmod p (zdrop z (zdrop x l)) (zdrop z (zdrop y l))) *)
   intro. rewrite H2. unfold inlist in |- *.
(* Goal: permmod p (zdrop x (Nil Z)) (zdrop y (Nil Z)) *)
(* Goal: @eq nat (length Z l) O *)
(* Goal: forall (n : nat) (_ : forall (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat n (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l)) (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat (S n) (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l) *)
   simpl in |- *. left. reflexivity. assumption.
Qed.

Lemma until_mod_all :
 forall (p : nat) (x : Z),
 0 < p ->
 ~ Mod x 0 p -> exists y : Z, inlist Z y (until (pred p)) /\ Mod x y p.
Proof.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros.
(* Goal: @ex Z (fun y : Z => and (inlist Z y (until (Init.Nat.pred p))) (Mod x y p)) *)
   elim (zdiv_rem (Z_of_nat p) x).
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intro q. intros.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   elim H1. intro r. intros.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   elim H2. intros. elim H3. intros.
(* Goal: Z.lt Z0 r *)
(* Goal: Z.le r (Z.of_nat (Init.Nat.pred p)) *)
(* Goal: Mod x (Z.mul a r) p *)
(* Goal: Z.gt (Z.of_nat p) Z0 *)
(* Goal: Prime p *)
(* Goal: not (Mod a Z0 p) *)
   elim (Zle_lt_or_eq 0 r).

   (* case 0 < r *)
(* Goal: not (@eq Z z y) *)
(* Goal: inlist Z z l *)
(* Goal: and (Mod z z p) (permmod p (zdrop z (zdrop x l)) (zdrop z (zdrop y l))) *)
   intro. split with r. split.
(* Goal: and (Mod x y p) (permmod p (zdrop x l0) (zdrop y l1)) *)
(* Goal: inlist Z x l0 *)
   apply until_ok. split.
(* Goal: not (Mod a Z0 p) *)
   assumption.
(* Goal: Z.le r (Z.of_nat (Init.Nat.pred p)) *)
(* Goal: Mod x (Z.mul a r) p *)
(* Goal: Z.gt (Z.of_nat p) Z0 *)
(* Goal: Prime p *)
(* Goal: not (Mod a Z0 p) *)
   apply Zlt_succ_le. rewrite <- Znat.inj_S. rewrite <- (S_pred p 0).
(* Goal: not (Mod a Z0 p) *)
   assumption. assumption.
(* Goal: not (Mod a Z0 p) *)
   split with q. rewrite Zplus_comm. rewrite Zmult_comm. assumption.

   (* case 0 = r *)
(* Goal: @ex Z (fun x1 : Z => and (inlist Z x1 l2) (and (Mod x0 x1 p) (permmod p (zdrop x0 l0) (zdrop x1 l2)))) *)
(* Goal: inlist Z x0 l0 *)
   intro. elim H0. split with q.
(* Goal: not (Mod a Z0 p) *)
   rewrite H7. rewrite Zplus_comm. rewrite Zmult_comm. assumption.

(* Goal: not (Mod a Z0 p) *)
   assumption.
(* Goal: not (Mod a Z0 p) *)
   change (Z_of_nat p > Z_of_nat 0)%Z in |- *. apply Znat.inj_gt. assumption.
Qed.

Lemma until_pos : forall (n : nat) (x : Z), inlist Z x (until n) -> (0 < x)%Z.
Proof.
(* Goal: forall (n p : nat) (l0 l1 : Zlist) (_ : @eq nat n (length Z l0)) (_ : @eq nat n (length Z l1)) (_ : Prime p) (_ : @eq nat (length Z l0) (length Z l1)) (_ : nodoubles p l0) (_ : allex p l0 l1), permmod p l0 l1 *)
   simple induction n.
(* Goal: permmod p (zdrop x (Nil Z)) (zdrop y (Nil Z)) *)
(* Goal: @eq nat (length Z l) O *)
(* Goal: forall (n : nat) (_ : forall (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat n (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l)) (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat (S n) (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l) *)
   unfold inlist in |- *. simpl in |- *. intros. elim H.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros m IH. intros. unfold inlist in H. simpl in H. elim H. intros.
(* Goal: permmod p (zdrop x (Nil Z)) (zdrop y (Nil Z)) *)
(* Goal: @eq nat (length Z l) O *)
(* Goal: forall (n : nat) (_ : forall (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat n (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l)) (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat (S n) (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l) *)
   rewrite H0. unfold Zlt in |- *. simpl in |- *. reflexivity.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros. apply IH. assumption.
Qed.

Lemma until_le_n :
 forall (n : nat) (x : Z), inlist Z x (until n) -> (x <= Z_of_nat n)%Z.
Proof.
(* Goal: forall (n p : nat) (l0 l1 : Zlist) (_ : @eq nat n (length Z l0)) (_ : @eq nat n (length Z l1)) (_ : Prime p) (_ : @eq nat (length Z l0) (length Z l1)) (_ : nodoubles p l0) (_ : allex p l0 l1), permmod p l0 l1 *)
   simple induction n.
(* Goal: permmod p (zdrop x (Nil Z)) (zdrop y (Nil Z)) *)
(* Goal: @eq nat (length Z l) O *)
(* Goal: forall (n : nat) (_ : forall (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat n (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l)) (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat (S n) (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l) *)
   unfold inlist in |- *. simpl in |- *. intros. elim H.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros m IH. intros. unfold inlist in H. simpl in H. elim H. intros.
(* Goal: Mod (Z.mul ra x) (Z.mul (Z.mul a r) ra) p *)
(* Goal: Z.gt (Z.of_nat p) Z0 *)
(* Goal: Prime p *)
(* Goal: not (Mod a Z0 p) *)
   rewrite H0. apply Zle_refl.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros. apply Zle_trans with (Z_of_nat m).
(* Goal: not (Mod a Z0 p) *)
   apply IH. assumption. apply Znat.inj_le. apply le_S. apply le_n.
Qed.

Lemma until_not_0mod :
 forall (p : nat) (x : Z),
 0 < p -> inlist Z x (until (pred p)) -> ~ Mod x 0 p.
Proof.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros. apply mod_repr_non_0. split.
(* Goal: not (Mod a Z0 p) *)
   apply (until_pos (pred p) x). assumption.
(* Goal: Z.lt x (Z.of_nat p) *)
   rewrite (S_pred p 0). rewrite Znat.inj_S.
(* Goal: Z.lt x (Z.succ (Z.of_nat m)) *)
(* Goal: Z.le (Z.of_nat (S m)) x *)
(* Goal: nodoubles p (until m) *)
   apply Zle_lt_succ. apply until_le_n.
(* Goal: not (Mod a Z0 p) *)
   assumption. assumption.
Qed.

Lemma untiln_prod_not_0modp :
 forall p n : nat,
 0 < n -> n < p -> Prime p -> ~ Mod (zproduct (until n)) 0 p.
Proof.
(* Goal: forall (n p : nat) (l0 l1 : Zlist) (_ : @eq nat n (length Z l0)) (_ : @eq nat n (length Z l1)) (_ : Prime p) (_ : @eq nat (length Z l0) (length Z l1)) (_ : nodoubles p l0) (_ : allex p l0 l1), permmod p l0 l1 *)
   simple induction n.
(* Goal: not (Mod a Z0 p) *)
   intro. elim (lt_irrefl 0). assumption.
(* Goal: forall (n : nat) (_ : forall (_ : lt O n) (_ : lt n p) (_ : Prime p), not (Mod (zproduct (until n)) Z0 p)) (_ : lt O (S n)) (_ : lt (S n) p) (_ : Prime p), not (Mod (zproduct (until (S n))) Z0 p) *)
   intros m IH H0m Hmp Hp.
(* Goal: not (Mod (zproduct (until (S m))) Z0 p) *)
   change (~ Mod (Z_of_nat (S m) * zproduct (until m)) 0 p) in |- *.
(* Goal: not (@eq Z z y) *)
(* Goal: inlist Z z l *)
(* Goal: and (Mod z z p) (permmod p (zdrop z (zdrop x l)) (zdrop z (zdrop y l))) *)
   intro. elim (mod_mult_0 p (Z_of_nat (S m)) (zproduct (until m))).
(* Goal: not (@eq Z z y) *)
(* Goal: inlist Z z l *)
(* Goal: and (Mod z z p) (permmod p (zdrop z (zdrop x l)) (zdrop z (zdrop y l))) *)
   intro. elim (mod_repr_non_0 p (Z_of_nat (S m))). split.
(* Goal: Z.lt Z0 (Z.of_nat (S m)) *)
(* Goal: Z.lt (Z.of_nat (S m)) (Z.of_nat p) *)
(* Goal: and (Z.lt Z0 x) (Z.lt x (Z.of_nat p)) *)
(* Goal: Mod (Z.of_nat (S m)) x p *)
(* Goal: nodoubles p (until m) *)
   change (Z_of_nat 0 < Z_of_nat (S m))%Z in |- *.
(* Goal: not (Mod a Z0 p) *)
   apply Znat.inj_lt. assumption.
(* Goal: not (Mod a Z0 p) *)
   apply Znat.inj_lt. assumption.
(* Goal: not (Mod a Z0 p) *)
   assumption.
(* Goal: not (@eq Z z y) *)
(* Goal: inlist Z z l *)
(* Goal: and (Mod z z p) (permmod p (zdrop z (zdrop x l)) (zdrop z (zdrop y l))) *)
   intro. elim (le_lt_or_eq 0 m). intro.
(* Goal: not (Mod a Z0 p) *)
   elim IH. assumption. apply lt_trans with (S m).
(* Goal: not (Mod a Z0 p) *)
   apply lt_n_Sn. assumption. assumption.
(* Goal: not (Mod a Z0 p) *)
   assumption. intro. rewrite <- H1 in H. simpl in H.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   elim mod_0not1 with p. elim Hp. intros. assumption.
(* Goal: not (Mod a Z0 p) *)
   apply mod_sym. assumption.
(* Goal: not (Mod a Z0 p) *)
   apply le_O_n. assumption.
(* Goal: not (Mod a Z0 p) *)
   assumption.
Qed.

Lemma until_prod_not_0mod :
 forall p : nat, Prime p -> ~ Mod (zproduct (until (pred p))) 0 p.
Proof.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros. elim H. intros.
(* Goal: not (Mod (zproduct (until (Init.Nat.pred p))) Z0 p) *)
   apply untiln_prod_not_0modp; auto with arith.
Qed.

Lemma until_mapmult_exp :
 forall (a : Z) (n : nat),
 zproduct (mapmult a (until n)) = (Exp a n * zproduct (until n))%Z.
Proof.
(* Goal: forall (n p : nat) (l0 l1 : Zlist) (_ : @eq nat n (length Z l0)) (_ : @eq nat n (length Z l1)) (_ : Prime p) (_ : @eq nat (length Z l0) (length Z l1)) (_ : nodoubles p l0) (_ : allex p l0 l1), permmod p l0 l1 *)
   simple induction n.
(* Goal: permmod p (zdrop x (Nil Z)) (zdrop y (Nil Z)) *)
(* Goal: @eq nat (length Z l) O *)
(* Goal: forall (n : nat) (_ : forall (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat n (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l)) (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat (S n) (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l) *)
   simpl in |- *. reflexivity.
(* Goal: forall (n : nat) (_ : forall (p : nat) (l0 l1 : Zlist) (_ : @eq nat n (length Z l0)) (_ : @eq nat n (length Z l1)) (_ : Prime p) (_ : @eq nat (length Z l0) (length Z l1)) (_ : nodoubles p l0) (_ : allex p l0 l1), permmod p l0 l1) (p : nat) (l0 l1 : Zlist) (_ : @eq nat (S n) (length Z l0)) (_ : @eq nat (S n) (length Z l1)) (_ : Prime p) (_ : @eq nat (length Z l0) (length Z l1)) (_ : nodoubles p l0) (_ : allex p l0 l1), permmod p l0 l1 *)
   intros m IH.
   replace (mapmult a (until (S m))) with
    (Cons Z (a * Z_of_nat (S m))%Z (mapmult a (until m))).
(* Goal: @eq Z (zproduct (Cons Z (Z.mul a (Z.of_nat (S m))) (mapmult a (until m)))) (Z.mul (Exp a (S m)) (zproduct (until (S m)))) *)
(* Goal: @eq (list Z) (Cons Z (Z.mul a (Z.of_nat (S m))) (mapmult a (until m))) (mapmult a (until (S m))) *)
   rewrite exp_S.
   replace (zproduct (Cons Z (a * Z_of_nat (S m))%Z (mapmult a (until m))))
    with (a * Z_of_nat (S m) * zproduct (mapmult a (until m)))%Z.
(* Goal: @eq Z (Z.mul (Z.mul a (Z.of_nat (S m))) (zproduct (mapmult a (until m)))) (Z.mul (Z.mul a (Exp a m)) (zproduct (until (S m)))) *)
(* Goal: @eq Z (Z.mul (Z.mul a (Z.of_nat (S m))) (zproduct (mapmult a (until m)))) (zproduct (Cons Z (Z.mul a (Z.of_nat (S m))) (mapmult a (until m)))) *)
(* Goal: @eq (list Z) (Cons Z (Z.mul a (Z.of_nat (S m))) (mapmult a (until m))) (mapmult a (until (S m))) *)
   rewrite IH. rewrite Zmult_assoc_reverse.
(* Goal: @eq Z (Z.mul a (Z.mul (Z.of_nat (S m)) (Z.mul (Exp a m) (zproduct (until m))))) (Z.mul (Z.mul a (Exp a m)) (zproduct (until (S m)))) *)
(* Goal: @eq Z (Z.mul (Z.mul a (Z.of_nat (S m))) (zproduct (mapmult a (until m)))) (zproduct (Cons Z (Z.mul a (Z.of_nat (S m))) (mapmult a (until m)))) *)
(* Goal: @eq (list Z) (Cons Z (Z.mul a (Z.of_nat (S m))) (mapmult a (until m))) (mapmult a (until (S m))) *)
   rewrite (Zmult_assoc (Z_of_nat (S m)) (Exp a m)).
(* Goal: @eq Z (Z.mul a (Z.mul (Z.mul (Z.of_nat (S m)) (Exp a m)) (zproduct (until m)))) (Z.mul (Z.mul a (Exp a m)) (zproduct (until (S m)))) *)
(* Goal: @eq Z (Z.mul (Z.mul a (Z.of_nat (S m))) (zproduct (mapmult a (until m)))) (zproduct (Cons Z (Z.mul a (Z.of_nat (S m))) (mapmult a (until m)))) *)
(* Goal: @eq (list Z) (Cons Z (Z.mul a (Z.of_nat (S m))) (mapmult a (until m))) (mapmult a (until (S m))) *)
   rewrite (Zmult_comm (Z_of_nat (S m))).
(* Goal: @eq Z (Z.mul (Z.mul q (Z.of_nat p)) a) (Z.mul (Z.of_nat p) (Z.mul q a)) *)
(* Goal: Z.le Z0 r *)
(* Goal: Z.le r (Z.of_nat (Init.Nat.pred p)) *)
(* Goal: Mod x (Z.mul a r) p *)
(* Goal: Z.gt (Z.of_nat p) Z0 *)
(* Goal: Prime p *)
(* Goal: not (Mod a Z0 p) *)
   rewrite Zmult_assoc. rewrite Zmult_assoc.
   replace (zproduct (until (S m))) with
    (Z_of_nat (S m) * zproduct (until m))%Z.
(* Goal: @eq nat (length Z l0) (length Z l0) *)
(* Goal: @eq nat (length Z l0) (length Z l1) *)
(* Goal: Prime p *)
(* Goal: @eq nat (length Z l0) (length Z l1) *)
(* Goal: nodoubles p l0 *)
(* Goal: allex p l0 l1 *)
   rewrite Zmult_assoc. reflexivity.
(* Goal: @eq nat (length Z l0) (length Z l0) *)
(* Goal: @eq nat (length Z l0) (length Z l1) *)
(* Goal: Prime p *)
(* Goal: @eq nat (length Z l0) (length Z l1) *)
(* Goal: nodoubles p l0 *)
(* Goal: allex p l0 l1 *)
   reflexivity. reflexivity. reflexivity.
Qed.

Lemma until_mapmult_allex :
 forall (p : nat) (a : Z),
 Prime p ->
 ~ Mod a 0 p -> allex p (until (pred p)) (mapmult a (until (pred p))).
Proof.
(* Goal: allex p (until (Init.Nat.pred p)) (mapmult a (until (Init.Nat.pred p))) *)
   unfold allex in |- *.
(* Goal: forall (p : nat) (a : Z) (_ : Prime p) (_ : not (Mod a Z0 p)) (x : Z) (_ : inlist Z x (until (Init.Nat.pred p))), @ex Z (fun y : Z => and (inlist Z y (mapmult a (until (Init.Nat.pred p)))) (Mod x y p)) *)
   intros p a Hprime Ha0 x Hx. elim Hprime. intros Hp Hp1.
(* Goal: @ex Z (fun y : Z => and (inlist Z y (mapmult a (until (Init.Nat.pred p)))) (Mod x y p)) *)
   elim (mod_mult_inv_r a p). intros ra Hra.
(* Goal: @ex Z (fun y : Z => and (inlist Z y (mapmult a (until (Init.Nat.pred p)))) (Mod x y p)) *)
(* Goal: Prime p *)
(* Goal: not (Mod a Z0 p) *)
   elim (zdiv_rem (Z_of_nat p) (ra * x)). intros q Hq. elim Hq.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros r Hr. elim Hr. intros. elim H. intros.
(* Goal: @ex Z (fun y : Z => and (inlist Z y (mapmult a (until (Init.Nat.pred p)))) (Mod x y p)) *)
(* Goal: Z.gt (Z.of_nat p) Z0 *)
(* Goal: Prime p *)
(* Goal: not (Mod a Z0 p) *)
   split with (a * r)%Z.
(* Goal: and (Mod x y p) (permmod p (zdrop x l0) (zdrop y l1)) *)
(* Goal: inlist Z x l0 *)
   split. apply mapmult_image. apply until_ok.
(* Goal: not (Mod a Z0 p) *)
   split. elim (Zle_lt_or_eq 0 r). intro. assumption.
(* Goal: not (@eq Z z y) *)
(* Goal: inlist Z z l *)
(* Goal: and (Mod z z p) (permmod p (zdrop z (zdrop x l)) (zdrop z (zdrop y l))) *)
   intro. rewrite <- H3 in H0. rewrite <- Zplus_0_r_reverse in H0.
(* Goal: Z.lt Z0 r *)
(* Goal: Z.le Z0 r *)
(* Goal: Z.le r (Z.of_nat (Init.Nat.pred p)) *)
(* Goal: Mod x (Z.mul a r) p *)
(* Goal: Z.gt (Z.of_nat p) Z0 *)
(* Goal: Prime p *)
(* Goal: not (Mod a Z0 p) *)
   elim until_not_0mod with p x.
(* Goal: not (Mod a Z0 p) *)
   apply lt_trans with 1. apply lt_n_Sn. assumption.
(* Goal: not (Mod a Z0 p) *)
   assumption.
(* Goal: not (Mod a Z0 p) *)
   apply mod_mult_cancel_r with (a * ra)%Z. assumption.
(* Goal: not (Mod a Z0 p) *)
   intro. elim mod_0not1 with p. assumption.
(* Goal: not (Mod a Z0 p) *)
   apply mod_trans with (a * ra)%Z. apply mod_sym. assumption. assumption.
(* Goal: @eq Z (Z.mul (Z.mul q (Z.of_nat p)) a) (Z.mul (Z.of_nat p) (Z.mul q a)) *)
(* Goal: Z.le Z0 r *)
(* Goal: Z.le r (Z.of_nat (Init.Nat.pred p)) *)
(* Goal: Mod x (Z.mul a r) p *)
(* Goal: Z.gt (Z.of_nat p) Z0 *)
(* Goal: Prime p *)
(* Goal: not (Mod a Z0 p) *)
   rewrite (Zmult_comm a ra). rewrite Zmult_assoc. rewrite (Zmult_comm x ra).
(* Goal: permmod p (zdrop x (Nil Z)) (zdrop y (Nil Z)) *)
(* Goal: @eq nat (length Z l) O *)
(* Goal: forall (n : nat) (_ : forall (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat n (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l)) (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat (S n) (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l) *)
   rewrite H0. simpl in |- *. unfold Mod in |- *. split with (q * a)%Z. simpl in |- *.
(* Goal: @eq nat (length Z l0) (length Z l0) *)
(* Goal: @eq nat (length Z l0) (length Z l1) *)
(* Goal: Prime p *)
(* Goal: @eq nat (length Z l0) (length Z l1) *)
(* Goal: nodoubles p l0 *)
(* Goal: allex p l0 l1 *)
   rewrite Zmult_assoc. rewrite (Zmult_comm q). reflexivity.
(* Goal: not (Mod a Z0 p) *)
   assumption. apply Zlt_succ_le.
(* Goal: not (Mod a Z0 p) *)
   rewrite <- Znat.inj_S. rewrite <- (S_pred p 1). assumption.
(* Goal: not (Mod a Z0 p) *)
   assumption.
(* Goal: not (Mod a Z0 p) *)
   apply mod_mult_cancel_r with ra. assumption.
(* Goal: not (Mod a Z0 p) *)
   intro. elim mod_0not1 with p. assumption.
(* Goal: Mod Z0 (Zpos xH) p *)
(* Goal: Mod (Z.mul x ra) (Z.mul (Z.mul a r) ra) p *)
(* Goal: Z.gt (Z.of_nat p) Z0 *)
(* Goal: Prime p *)
(* Goal: not (Mod a Z0 p) *)
   apply mod_trans with (ra * a)%Z. change (Mod (0 * a) (ra * a) p) in |- *.
(* Goal: not (Mod a Z0 p) *)
   apply mod_mult_compat. apply mod_sym. assumption.
(* Goal: not (Mod a Z0 p) *)
   apply mod_refl. rewrite (Zmult_comm ra a). assumption.
(* Goal: Mod (Z.mul ra x) (Z.mul (Z.mul a r) ra) p *)
(* Goal: Z.gt (Z.of_nat p) Z0 *)
(* Goal: Prime p *)
(* Goal: not (Mod a Z0 p) *)
   rewrite (Zmult_comm x ra). rewrite H0.
(* Goal: Mod (Z.add (Z.mul q (Z.of_nat p)) r) (Z.mul (Z.mul a r) ra) p *)
(* Goal: Z.gt (Z.of_nat p) Z0 *)
(* Goal: Prime p *)
(* Goal: not (Mod a Z0 p) *)
   rewrite (Zmult_comm a r). rewrite (Zmult_assoc_reverse r a ra).
(* Goal: Mod (Z.add (Z.mul q (Z.of_nat p)) r) r p *)
(* Goal: Mod r (Z.mul r (Z.mul a ra)) p *)
(* Goal: Z.gt (Z.of_nat p) Z0 *)
(* Goal: Prime p *)
(* Goal: not (Mod a Z0 p) *)
   apply mod_trans with r. split with q.
(* Goal: @eq nat (length Z l0) (length Z l0) *)
(* Goal: @eq nat (length Z l0) (length Z l1) *)
(* Goal: Prime p *)
(* Goal: @eq nat (length Z l0) (length Z l1) *)
(* Goal: nodoubles p l0 *)
(* Goal: allex p l0 l1 *)
   rewrite Zplus_comm. rewrite Zmult_comm. reflexivity.
(* Goal: Mod r (Z.mul r (Z.mul a ra)) p *)
(* Goal: Z.gt (Z.of_nat p) Z0 *)
(* Goal: Prime p *)
(* Goal: not (Mod a Z0 p) *)
   pattern r at 1 in |- *. rewrite <- Zmult_1_l with r.
(* Goal: Mod (Z.mul h (zproduct t)) (Z.mul x (zproduct (zdrop x l1))) p *)
(* Goal: inlist Z x l1 *)
   rewrite (Zmult_comm 1 r). apply mod_mult_compat.
(* Goal: not (Mod a Z0 p) *)
   apply mod_refl. apply mod_sym. assumption.
(* Goal: Z.gt (Z.of_nat p) Z0 *)
(* Goal: Prime p *)
(* Goal: not (Mod a Z0 p) *)
   change (Z_of_nat p > Z_of_nat 0)%Z in |- *. apply Znat.inj_gt.
(* Goal: not (Mod a Z0 p) *)
   apply gt_trans with 1. assumption. apply gt_Sn_n.
(* Goal: not (Mod a Z0 p) *)
   assumption. assumption.
Qed.

Lemma until_nodoubles1 :
 forall p : nat, Prime p -> forall n : nat, n < p -> nodoubles p (until n).
Proof.
(* Goal: forall (n p : nat) (l0 l1 : Zlist) (_ : @eq nat n (length Z l0)) (_ : @eq nat n (length Z l1)) (_ : Prime p) (_ : @eq nat (length Z l0) (length Z l1)) (_ : nodoubles p l0) (_ : allex p l0 l1), permmod p l0 l1 *)
   simple induction n.
(* Goal: permmod p (zdrop x (Nil Z)) (zdrop y (Nil Z)) *)
(* Goal: @eq nat (length Z l) O *)
(* Goal: forall (n : nat) (_ : forall (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat n (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l)) (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat (S n) (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l) *)
   intros. simpl in |- *. apply nodoubles_nil.
(* Goal: forall (n : nat) (_ : forall _ : lt n p, nodoubles p (until n)) (_ : lt (S n) p), nodoubles p (until (S n)) *)
   intros m IH Hb.
(* Goal: nodoubles p (until (S m)) *)
   change (nodoubles p (Cons Z (Z_of_nat (S m)) (until m))) in |- *.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   apply nodoubles_ind. intros.
(* Goal: not (@eq Z z y) *)
(* Goal: inlist Z z l *)
(* Goal: and (Mod z z p) (permmod p (zdrop z (zdrop x l)) (zdrop z (zdrop y l))) *)
   intro. elim (Zlt_not_le x (Z_of_nat (S m))).
(* Goal: Z.lt x (Z.of_nat (S m)) *)
(* Goal: Z.le (Z.of_nat (S m)) x *)
(* Goal: nodoubles p (until m) *)
   rewrite Znat.inj_S. apply Zle_lt_succ. apply until_le_n.
(* Goal: not (Mod a Z0 p) *)
   assumption. apply Zeq_le. apply mod_repr_eq with p.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   elim H. intros. apply lt_trans with 1. apply lt_n_Sn. assumption.
(* Goal: and (Mod x y p) (permmod p (zdrop x l0) (zdrop y l1)) *)
(* Goal: inlist Z x l0 *)
   split. change (Z_of_nat 0 < Z_of_nat (S m))%Z in |- *. apply Znat.inj_lt.
(* Goal: not (Mod a Z0 p) *)
   apply lt_O_Sn. apply Znat.inj_lt. assumption.
(* Goal: not (Mod a Z0 p) *)
   split. apply until_pos with m. assumption.
(* Goal: Z.lt x (Z.of_nat p) *)
(* Goal: Mod (Z.of_nat (S m)) x p *)
(* Goal: nodoubles p (until m) *)
   apply Zle_lt_trans with (Z_of_nat m).
(* Goal: not (Mod a Z0 p) *)
   apply until_le_n. assumption.
(* Goal: Z.lt (Z.of_nat m) (Z.of_nat p) *)
(* Goal: Mod (Z.of_nat (S m)) x p *)
(* Goal: nodoubles p (until m) *)
   apply Znat.inj_lt. apply le_lt_trans with (S m).
(* Goal: not (Mod a Z0 p) *)
   apply le_n_Sn. assumption.
(* Goal: not (Mod a Z0 p) *)
   assumption.
(* Goal: permmod p (zdrop x l0) (zdrop y l1) *)
(* Goal: inlist Z x l0 *)
   apply IH. apply le_lt_trans with (S m).
(* Goal: not (Mod a Z0 p) *)
   apply le_n_Sn. assumption.
Qed.

Lemma until_nodoubles :
 forall p : nat, Prime p -> nodoubles p (until (pred p)).
Proof.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros. apply until_nodoubles1. assumption.
(* Goal: lt O p *)
   apply lt_pred_n_n. apply lt_trans with 1.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   apply lt_n_Sn. elim H. intros. assumption.
Qed.

(** * Permutations modulo p. *)

Fixpoint permmod (p : nat) (l1 : Zlist) {struct l1} : 
 Zlist -> Prop :=
  fun l2 : Zlist =>
  match l1 with
  | Nil => l2 = Nil Z
  | Cons x t =>
      exists y : Z, inlist Z y l2 /\ Mod x y p /\ permmod p t (zdrop y l2)
  end.

Lemma permmod_nil : forall p : nat, permmod p (Nil Z) (Nil Z).
Proof.
(* Goal: permmod p (zdrop x (Nil Z)) (zdrop y (Nil Z)) *)
(* Goal: @eq nat (length Z l) O *)
(* Goal: forall (n : nat) (_ : forall (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat n (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l)) (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat (S n) (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l) *)
   simpl in |- *. intro. reflexivity.
Qed.

Lemma permmod_drop :
 forall (p : nat) (x1 x2 : Z) (l1 l2 : Zlist),
 Mod x1 x2 p ->
 inlist Z x1 l1 ->
 inlist Z x2 l2 -> permmod p (zdrop x1 l1) (zdrop x2 l2) -> permmod p l1 l2.
Proof.
(* Goal: forall (l1 : Zlist) (_ : @eq nat (length Z (Nil Z)) (length Z l1)) (_ : forall (x0 : Z) (_ : inlist Z x0 (Nil Z)), @ex Z (fun x1 : Z => and (inlist Z x1 l1) (and (Mod x0 x1 p) (permmod p (zdrop x0 (Nil Z)) (zdrop x1 l1))))), permmod p (Nil Z) l1 *)
(* Goal: forall (a : Z) (l : list Z) (_ : forall (l1 : Zlist) (_ : @eq nat (length Z l) (length Z l1)) (_ : forall (x0 : Z) (_ : inlist Z x0 l), @ex Z (fun x1 : Z => and (inlist Z x1 l1) (and (Mod x0 x1 p) (permmod p (zdrop x0 l) (zdrop x1 l1))))), permmod p l l1) (l1 : Zlist) (_ : @eq nat (length Z (Cons Z a l)) (length Z l1)) (_ : forall (x0 : Z) (_ : inlist Z x0 (Cons Z a l)), @ex Z (fun x1 : Z => and (inlist Z x1 l1) (and (Mod x0 x1 p) (permmod p (zdrop x0 (Cons Z a l)) (zdrop x1 l1))))), permmod p (Cons Z a l) l1 *)
   simple induction l1.
(* Goal: permmod p (zdrop x (Nil Z)) (zdrop y (Nil Z)) *)
(* Goal: @eq nat (length Z l) O *)
(* Goal: forall (n : nat) (_ : forall (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat n (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l)) (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat (S n) (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l) *)
   simpl in |- *. intros. elim H0.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (l1 : Zlist) (p : nat) (_ : permmod p l l1), Mod (zproduct l) (zproduct l1) p) (l1 : Zlist) (p : nat) (_ : permmod p (Cons Z a l) l1), Mod (zproduct (Cons Z a l)) (zproduct l1) p *)
   intros h t IH. intros l2 Hm.
(* Goal: forall (_ : inlist Z x1 (Cons Z h t)) (_ : inlist Z x2 l2) (_ : permmod p (zdrop x1 (Cons Z h t)) (zdrop x2 l2)), permmod p (Cons Z h t) l2 *)
   elim (zeqdec x1 h).
(* Goal: permmod p (zdrop x (Nil Z)) (zdrop y (Nil Z)) *)
(* Goal: @eq nat (length Z l) O *)
(* Goal: forall (n : nat) (_ : forall (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat n (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l)) (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat (S n) (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l) *)
   intros. simpl in |- *. split with x2.
(* Goal: not (Mod a Z0 p) *)
   split. assumption.
(* Goal: not (Mod a Z0 p) *)
   split. rewrite <- H. assumption.
(* Goal: permmod p t (zdrop x2 l2) *)
(* Goal: forall (_ : not (@eq Z x1 h)) (_ : inlist Z x1 (Cons Z h t)) (_ : inlist Z x2 l2) (_ : permmod p (zdrop x1 (Cons Z h t)) (zdrop x2 l2)), permmod p (Cons Z h t) l2 *)
   rewrite H in H2. rewrite zdrop_head_eq in H2.
(* Goal: not (Mod a Z0 p) *)
   assumption. reflexivity.
(* Goal: not (@eq Z z y) *)
(* Goal: inlist Z z l *)
(* Goal: and (Mod z z p) (permmod p (zdrop z (zdrop x l)) (zdrop z (zdrop y l))) *)
   intro.
(* Goal: permmod p (zdrop x (Cons Z h0 t0)) (zdrop y l1) *)
(* Goal: inlist Z x t0 *)
   rewrite zdrop_head_neq.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros. elim H2. intros y Hy.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   elim Hy. intros. elim H4. intros.
(* Goal: @ex Z (fun x1 : Z => and (inlist Z x1 l1) (and (Mod x x1 p) (permmod p (zdrop x l0) (zdrop x1 l1)))) *)
(* Goal: inlist Z x l0 *)
   split with y. split.
(* Goal: not (Mod a Z0 p) *)
   apply zdrop_inlist_weak with x2. assumption.
(* Goal: not (Mod a Z0 p) *)
   split. assumption.
(* Goal: permmod p t (zdrop y l2) *)
(* Goal: not (@eq Z x1 h) *)
   rewrite zdrop_swap in H6.
(* Goal: not (Mod a Z0 p) *)
   apply IH. assumption.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   elim (inlist_head_neq Z x1 h t). intros. apply H7. assumption.
(* Goal: not (Mod a Z0 p) *)
   assumption.
(* Goal: inlist Z x2 (zdrop y l2) *)
(* Goal: permmod p (zdrop x1 t) (zdrop x2 (zdrop y l2)) *)
(* Goal: not (@eq Z x1 h) *)
   elim (zeqdec x2 y).
(* Goal: not (Mod a Z0 p) *)
   intro. rewrite H7. rewrite H7 in H3. assumption.
(* Goal: not (Mod a Z0 p) *)
   intro. apply zdrop_neq_inlist. assumption. assumption.
(* Goal: not (Mod a Z0 p) *)
   assumption. assumption.
Qed.

Lemma permmod_drop_cons :
 forall (p : nat) (x1 x2 : Z) (t1 l2 : Zlist),
 Mod x1 x2 p ->
 inlist Z x2 l2 -> permmod p t1 (zdrop x2 l2) -> permmod p (Cons Z x1 t1) l2.
Proof.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros. apply permmod_drop with x1 x2.
(* Goal: not (Mod a Z0 p) *)
   assumption.
(* Goal: @eq nat (length Z l0) (length Z l0) *)
(* Goal: @eq nat (length Z l0) (length Z l1) *)
(* Goal: Prime p *)
(* Goal: @eq nat (length Z l0) (length Z l1) *)
(* Goal: nodoubles p l0 *)
(* Goal: allex p l0 l1 *)
   apply inlist_head_eq. reflexivity.
(* Goal: not (Mod a Z0 p) *)
   assumption.
(* Goal: not (Mod a Z0 p) *)
   rewrite zdrop_head_eq. assumption.
(* Goal: @eq nat (length Z l0) (length Z l0) *)
(* Goal: @eq nat (length Z l0) (length Z l1) *)
(* Goal: Prime p *)
(* Goal: @eq nat (length Z l0) (length Z l1) *)
(* Goal: nodoubles p l0 *)
(* Goal: allex p l0 l1 *)
   reflexivity.
Qed.

Lemma permmod_cons_extend :
 forall (p : nat) (x1 x2 : Z) (l1 l2 : Zlist),
 permmod p l1 l2 -> Mod x1 x2 p -> permmod p (Cons Z x1 l1) (Cons Z x2 l2).
Proof.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros.
(* Goal: permmod p (Cons Z x1 l1) (Cons Z x2 l2) *)
   apply permmod_drop with x1 x2.
(* Goal: not (Mod a Z0 p) *)
   assumption.
(* Goal: @eq nat (length Z l0) (length Z l0) *)
(* Goal: @eq nat (length Z l0) (length Z l1) *)
(* Goal: Prime p *)
(* Goal: @eq nat (length Z l0) (length Z l1) *)
(* Goal: nodoubles p l0 *)
(* Goal: allex p l0 l1 *)
   apply inlist_head_eq. reflexivity.
(* Goal: @eq nat (length Z l0) (length Z l0) *)
(* Goal: @eq nat (length Z l0) (length Z l1) *)
(* Goal: Prime p *)
(* Goal: @eq nat (length Z l0) (length Z l1) *)
(* Goal: nodoubles p l0 *)
(* Goal: allex p l0 l1 *)
   apply inlist_head_eq. reflexivity.
(* Goal: permmod p (zdrop x (Cons Z h0 t0)) (zdrop h1 l1) *)
(* Goal: forall _ : not (@eq Z x h0), @ex Z (fun y : Z => and (inlist Z y l1) (and (Mod x y p) (permmod p (zdrop x (Cons Z h0 t0)) (zdrop y l1)))) *)
   rewrite zdrop_head_eq. rewrite zdrop_head_eq.
(* Goal: not (Mod a Z0 p) *)
   assumption. reflexivity. reflexivity.
Qed.

Lemma permmod_length :
 forall (p : nat) (l1 l2 : Zlist),
 permmod p l1 l2 -> length Z l1 = length Z l2.
Proof.
(* Goal: forall (l1 : Zlist) (_ : @eq nat (length Z (Nil Z)) (length Z l1)) (_ : forall (x0 : Z) (_ : inlist Z x0 (Nil Z)), @ex Z (fun x1 : Z => and (inlist Z x1 l1) (and (Mod x0 x1 p) (permmod p (zdrop x0 (Nil Z)) (zdrop x1 l1))))), permmod p (Nil Z) l1 *)
(* Goal: forall (a : Z) (l : list Z) (_ : forall (l1 : Zlist) (_ : @eq nat (length Z l) (length Z l1)) (_ : forall (x0 : Z) (_ : inlist Z x0 l), @ex Z (fun x1 : Z => and (inlist Z x1 l1) (and (Mod x0 x1 p) (permmod p (zdrop x0 l) (zdrop x1 l1))))), permmod p l l1) (l1 : Zlist) (_ : @eq nat (length Z (Cons Z a l)) (length Z l1)) (_ : forall (x0 : Z) (_ : inlist Z x0 (Cons Z a l)), @ex Z (fun x1 : Z => and (inlist Z x1 l1) (and (Mod x0 x1 p) (permmod p (zdrop x0 (Cons Z a l)) (zdrop x1 l1))))), permmod p (Cons Z a l) l1 *)
   simple induction l1.
(* Goal: permmod p (zdrop x (Nil Z)) (zdrop y (Nil Z)) *)
(* Goal: @eq nat (length Z l) O *)
(* Goal: forall (n : nat) (_ : forall (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat n (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l)) (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat (S n) (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l) *)
   simpl in |- *. intros. rewrite H. simpl in |- *. reflexivity.
(* Goal: permmod p (zdrop x (Nil Z)) (zdrop y (Nil Z)) *)
(* Goal: @eq nat (length Z l) O *)
(* Goal: forall (n : nat) (_ : forall (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat n (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l)) (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat (S n) (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l) *)
   intros h t IH. simpl in |- *. intros.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   elim H. intros y Hy.  elim Hy. intros.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   elim H1. intros.
(* Goal: @eq nat (S (length Z t)) (length Z l2) *)
   rewrite (IH (zdrop y l2)).
(* Goal: @eq nat (S (length Z (zdrop y l2))) (length Z l2) *)
(* Goal: permmod p t (zdrop y l2) *)
   rewrite zdrop_length with y l2.
(* Goal: not (Mod a Z0 p) *)
   reflexivity. assumption. assumption.
Qed.

Lemma permmod_refl : forall (p : nat) (l : Zlist), permmod p l l.
Proof.
(* Goal: forall (p : nat) (l : Zlist), permmod p l l *)
   simple induction l.
(* Goal: permmod p (zdrop x (Nil Z)) (zdrop y (Nil Z)) *)
(* Goal: @eq nat (length Z l) O *)
(* Goal: forall (n : nat) (_ : forall (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat n (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l)) (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat (S n) (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l) *)
   simpl in |- *. reflexivity.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (l1 : Zlist) (p : nat) (_ : permmod p l l1), Mod (zproduct l) (zproduct l1) p) (l1 : Zlist) (p : nat) (_ : permmod p (Cons Z a l) l1), Mod (zproduct (Cons Z a l)) (zproduct l1) p *)
   intros h t IH. split with h.
(* Goal: and (Mod x y p) (permmod p (zdrop x l0) (zdrop y l1)) *)
(* Goal: inlist Z x l0 *)
   split. apply inlist_head_eq. reflexivity.
(* Goal: and (Mod x y p) (permmod p (zdrop x l0) (zdrop y l1)) *)
(* Goal: inlist Z x l0 *)
   split. apply mod_refl.
(* Goal: not (Mod a Z0 p) *)
   rewrite zdrop_head_eq. assumption. reflexivity.
Qed.

Lemma permmod_sym :
 forall (p : nat) (l1 l2 : Zlist), permmod p l1 l2 -> permmod p l2 l1.
Proof.
(* Goal: forall (l1 : Zlist) (_ : @eq nat (length Z (Nil Z)) (length Z l1)) (_ : forall (x0 : Z) (_ : inlist Z x0 (Nil Z)), @ex Z (fun x1 : Z => and (inlist Z x1 l1) (and (Mod x0 x1 p) (permmod p (zdrop x0 (Nil Z)) (zdrop x1 l1))))), permmod p (Nil Z) l1 *)
(* Goal: forall (a : Z) (l : list Z) (_ : forall (l1 : Zlist) (_ : @eq nat (length Z l) (length Z l1)) (_ : forall (x0 : Z) (_ : inlist Z x0 l), @ex Z (fun x1 : Z => and (inlist Z x1 l1) (and (Mod x0 x1 p) (permmod p (zdrop x0 l) (zdrop x1 l1))))), permmod p l l1) (l1 : Zlist) (_ : @eq nat (length Z (Cons Z a l)) (length Z l1)) (_ : forall (x0 : Z) (_ : inlist Z x0 (Cons Z a l)), @ex Z (fun x1 : Z => and (inlist Z x1 l1) (and (Mod x0 x1 p) (permmod p (zdrop x0 (Cons Z a l)) (zdrop x1 l1))))), permmod p (Cons Z a l) l1 *)
   simple induction l1.
(* Goal: permmod p (zdrop x (Nil Z)) (zdrop y (Nil Z)) *)
(* Goal: @eq nat (length Z l) O *)
(* Goal: forall (n : nat) (_ : forall (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat n (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l)) (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat (S n) (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l) *)
   simpl in |- *. intros. rewrite H. apply permmod_nil.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (l2 : Zlist) (_ : permmod p l l2), permmod p l2 l) (l2 : Zlist) (_ : permmod p (Cons Z a l) l2), permmod p l2 (Cons Z a l) *)
   intros h1 t1 IH1.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros. elim H. intros y Hy.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   elim Hy. intros. elim H1. intros.
(* Goal: permmod p l2 (Cons Z h1 t1) *)
   apply permmod_drop with y h1.
(* Goal: not (Mod a Z0 p) *)
   apply mod_sym. assumption.
(* Goal: not (Mod a Z0 p) *)
   assumption.
(* Goal: @eq nat (length Z l0) (length Z l0) *)
(* Goal: @eq nat (length Z l0) (length Z l1) *)
(* Goal: Prime p *)
(* Goal: @eq nat (length Z l0) (length Z l1) *)
(* Goal: nodoubles p l0 *)
(* Goal: allex p l0 l1 *)
   apply inlist_head_eq. reflexivity.
(* Goal: permmod p (zdrop x (Cons Z h0 t0)) (zdrop h1 l1) *)
(* Goal: forall _ : not (@eq Z x h0), @ex Z (fun y : Z => and (inlist Z y l1) (and (Mod x y p) (permmod p (zdrop x (Cons Z h0 t0)) (zdrop y l1)))) *)
   rewrite zdrop_head_eq. apply IH1.
(* Goal: not (Mod a Z0 p) *)
   assumption.
(* Goal: @eq nat (length Z l0) (length Z l0) *)
(* Goal: @eq nat (length Z l0) (length Z l1) *)
(* Goal: Prime p *)
(* Goal: @eq nat (length Z l0) (length Z l1) *)
(* Goal: nodoubles p l0 *)
(* Goal: allex p l0 l1 *)
   reflexivity.
Qed.

Lemma permmod_product :
 forall (l0 l1 : Zlist) (p : nat),
 permmod p l0 l1 -> Mod (zproduct l0) (zproduct l1) p.
Proof.
(* Goal: forall (p : nat) (l0 l1 : Zlist) (_ : permmod p l0 l1) (x : Z) (_ : inlist Z x l0), @ex Z (fun y : Z => and (inlist Z y l1) (and (Mod x y p) (permmod p (zdrop x l0) (zdrop y l1)))) *)
   simple induction l0.
(* Goal: permmod p (zdrop x (Nil Z)) (zdrop y (Nil Z)) *)
(* Goal: @eq nat (length Z l) O *)
(* Goal: forall (n : nat) (_ : forall (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat n (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l)) (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat (S n) (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l) *)
   simpl in |- *. intros. rewrite H. simpl in |- *. apply mod_refl.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros h t IH. intros.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   elim H. intros. elim H0. intros. elim H2. intros.
(* Goal: permmod p (zdrop x (Nil Z)) (zdrop y (Nil Z)) *)
(* Goal: @eq nat (length Z l) O *)
(* Goal: forall (n : nat) (_ : forall (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat n (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l)) (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat (S n) (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l) *)
   simpl in |- *. rewrite <- zdrop_product with x l1.
(* Goal: Mod (Z.mul h (zproduct t)) (Z.mul x (zproduct (zdrop x l1))) p *)
(* Goal: inlist Z x l1 *)
   apply mod_mult_compat.
(* Goal: not (Mod a Z0 p) *)
   assumption.
(* Goal: not (Mod a Z0 p) *)
   apply IH. assumption.
(* Goal: not (Mod a Z0 p) *)
   assumption.
Qed.

Lemma allex_permmod :
 forall (p : nat) (l0 l1 : Zlist),
 length Z l0 = length Z l1 ->
 (forall x0 : Z,
  inlist Z x0 l0 ->
  exists x1 : Z,
    inlist Z x1 l1 /\ Mod x0 x1 p /\ permmod p (zdrop x0 l0) (zdrop x1 l1)) ->
 permmod p l0 l1.
Proof.
(* Goal: forall (p : nat) (l0 l1 : Zlist) (_ : permmod p l0 l1) (x : Z) (_ : inlist Z x l0), @ex Z (fun y : Z => and (inlist Z y l1) (and (Mod x y p) (permmod p (zdrop x l0) (zdrop y l1)))) *)
   simple induction l0.
(* Goal: forall (l1 : Zlist) (_ : @eq nat (length Z (Nil Z)) (length Z l1)) (_ : forall (x0 : Z) (_ : inlist Z x0 (Nil Z)), @ex Z (fun x1 : Z => and (inlist Z x1 l1) (and (Mod x0 x1 p) (permmod p (zdrop x0 (Nil Z)) (zdrop x1 l1))))), permmod p (Nil Z) l1 *)
(* Goal: forall (a : Z) (l : list Z) (_ : forall (l1 : Zlist) (_ : @eq nat (length Z l) (length Z l1)) (_ : forall (x0 : Z) (_ : inlist Z x0 l), @ex Z (fun x1 : Z => and (inlist Z x1 l1) (and (Mod x0 x1 p) (permmod p (zdrop x0 l) (zdrop x1 l1))))), permmod p l l1) (l1 : Zlist) (_ : @eq nat (length Z (Cons Z a l)) (length Z l1)) (_ : forall (x0 : Z) (_ : inlist Z x0 (Cons Z a l)), @ex Z (fun x1 : Z => and (inlist Z x1 l1) (and (Mod x0 x1 p) (permmod p (zdrop x0 (Cons Z a l)) (zdrop x1 l1))))), permmod p (Cons Z a l) l1 *)
   simple induction l1.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros. apply permmod_nil.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros. discriminate H0.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros h0 t0 IH0. intros.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   elim (H0 h0). intro x1. intros.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   elim H1. intros. elim H3. intros.
(* Goal: permmod p (Cons Z h0 t0) l1 *)
(* Goal: inlist Z h0 (Cons Z h0 t0) *)
   rewrite zdrop_head_eq in H5.
(* Goal: permmod p (Cons Z h0 t0) l1 *)
(* Goal: @eq Z h0 h0 *)
(* Goal: inlist Z h0 (Cons Z h0 t0) *)
   apply permmod_drop_cons with x1.
(* Goal: not (Mod a Z0 p) *)
   assumption. assumption. assumption.
(* Goal: @eq nat (length Z l0) (length Z l0) *)
(* Goal: @eq nat (length Z l0) (length Z l1) *)
(* Goal: Prime p *)
(* Goal: @eq nat (length Z l0) (length Z l1) *)
(* Goal: nodoubles p l0 *)
(* Goal: allex p l0 l1 *)
   reflexivity.
(* Goal: @eq nat (length Z l0) (length Z l0) *)
(* Goal: @eq nat (length Z l0) (length Z l1) *)
(* Goal: Prime p *)
(* Goal: @eq nat (length Z l0) (length Z l1) *)
(* Goal: nodoubles p l0 *)
(* Goal: allex p l0 l1 *)
   apply inlist_head_eq. reflexivity.
Qed.

Lemma permmod_allex :
 forall (p : nat) (l0 l1 : Zlist),
 permmod p l0 l1 ->
 forall x : Z,
 inlist Z x l0 ->
 exists y : Z,
   inlist Z y l1 /\ Mod x y p /\ permmod p (zdrop x l0) (zdrop y l1).
Proof.
(* Goal: forall (p : nat) (l0 l1 : Zlist) (_ : permmod p l0 l1) (x : Z) (_ : inlist Z x l0), @ex Z (fun y : Z => and (inlist Z y l1) (and (Mod x y p) (permmod p (zdrop x l0) (zdrop y l1)))) *)
   simple induction l0.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros. elim H0.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros h0 t0 IH0. intros.
(* Goal: @ex Z (fun y : Z => and (inlist Z y l1) (and (Mod x y p) (permmod p (zdrop x (Cons Z h0 t0)) (zdrop y l1)))) *)
   elim H. intros h1 Hh1.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   elim Hh1. intros. elim H2. intros.
(* Goal: @ex Z (fun y : Z => and (inlist Z y l1) (and (Mod x y p) (permmod p (zdrop x (Cons Z h0 t0)) (zdrop y l1)))) *)
   elim (zeqdec x h0).
(* Goal: not (@eq Z z y) *)
(* Goal: inlist Z z l *)
(* Goal: and (Mod z z p) (permmod p (zdrop z (zdrop x l)) (zdrop z (zdrop y l))) *)
   intro. split with h1.
(* Goal: not (Mod a Z0 p) *)
   split. assumption.
(* Goal: not (Mod a Z0 p) *)
   split. rewrite H5. assumption.
(* Goal: not (Mod a Z0 p) *)
   rewrite zdrop_head_eq. assumption. assumption.
(* Goal: not (@eq Z z y) *)
(* Goal: inlist Z z l *)
(* Goal: and (Mod z z p) (permmod p (zdrop z (zdrop x l)) (zdrop z (zdrop y l))) *)
   intro. elim (IH0 (zdrop h1 l1) H4 x).
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros y Hy. elim Hy. intros. elim H7. intros.
(* Goal: @ex Z (fun x1 : Z => and (inlist Z x1 l1) (and (Mod x x1 p) (permmod p (zdrop x l0) (zdrop x1 l1)))) *)
(* Goal: inlist Z x l0 *)
   split with y.
(* Goal: not (Mod a Z0 p) *)
   split. apply zdrop_inlist_weak with h1. assumption.
(* Goal: not (Mod a Z0 p) *)
   split. assumption.
(* Goal: permmod p (zdrop x (Cons Z h0 t0)) (zdrop y l1) *)
(* Goal: inlist Z x t0 *)
   rewrite zdrop_head_neq. split with h1.
(* Goal: and (Mod x y p) (permmod p (zdrop x l0) (zdrop y l1)) *)
(* Goal: inlist Z x l0 *)
   split. elim (zeqdec h1 y).
(* Goal: not (Mod a Z0 p) *)
   intro. rewrite H10 in H6. rewrite H10. assumption.
(* Goal: not (Mod a Z0 p) *)
   intro. apply zdrop_neq_inlist. assumption. assumption.
(* Goal: not (Mod a Z0 p) *)
   split. assumption. rewrite zdrop_swap. assumption.
(* Goal: not (Mod a Z0 p) *)
   assumption. elim (inlist_head_neq Z x h0 t0).
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros. apply H6. assumption. assumption.
Qed.

Lemma permmod_trans1 :
 forall (n p : nat) (l0 l1 l2 : Zlist),
 length Z l0 = n ->
 length Z l1 = n ->
 length Z l2 = n -> permmod p l0 l1 -> permmod p l1 l2 -> permmod p l0 l2.
Proof.
(* Goal: forall (n p : nat) (l0 l1 : Zlist) (_ : @eq nat n (length Z l0)) (_ : @eq nat n (length Z l1)) (_ : Prime p) (_ : @eq nat (length Z l0) (length Z l1)) (_ : nodoubles p l0) (_ : allex p l0 l1), permmod p l0 l1 *)
   simple induction n.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros.
(* Goal: permmod p l0 l1 *)
(* Goal: forall (n : nat) (_ : forall (p : nat) (l0 l1 : Zlist) (_ : @eq nat n (length Z l0)) (_ : @eq nat n (length Z l1)) (_ : Prime p) (_ : @eq nat (length Z l0) (length Z l1)) (_ : nodoubles p l0) (_ : allex p l0 l1), permmod p l0 l1) (p : nat) (l0 l1 : Zlist) (_ : @eq nat (S n) (length Z l0)) (_ : @eq nat (S n) (length Z l1)) (_ : Prime p) (_ : @eq nat (length Z l0) (length Z l1)) (_ : nodoubles p l0) (_ : allex p l0 l1), permmod p l0 l1 *)
   rewrite length_0 with Z l0.
(* Goal: permmod p (Nil Z) l2 *)
(* Goal: @eq nat (length Z l0) O *)
(* Goal: forall (n : nat) (_ : forall (p : nat) (l0 l1 l2 : Zlist) (_ : @eq nat (length Z l0) n) (_ : @eq nat (length Z l1) n) (_ : @eq nat (length Z l2) n) (_ : permmod p l0 l1) (_ : permmod p l1 l2), permmod p l0 l2) (p : nat) (l0 l1 l2 : Zlist) (_ : @eq nat (length Z l0) (S n)) (_ : @eq nat (length Z l1) (S n)) (_ : @eq nat (length Z l2) (S n)) (_ : permmod p l0 l1) (_ : permmod p l1 l2), permmod p l0 l2 *)
   rewrite length_0 with Z l2.
(* Goal: not (Mod a Z0 p) *)
   apply permmod_nil. assumption. assumption.
(* Goal: forall (n : nat) (_ : forall (p : nat) (l0 l1 : Zlist) (_ : @eq nat n (length Z l0)) (_ : @eq nat n (length Z l1)) (_ : Prime p) (_ : @eq nat (length Z l0) (length Z l1)) (_ : nodoubles p l0) (_ : allex p l0 l1), permmod p l0 l1) (p : nat) (l0 l1 : Zlist) (_ : @eq nat (S n) (length Z l0)) (_ : @eq nat (S n) (length Z l1)) (_ : Prime p) (_ : @eq nat (length Z l0) (length Z l1)) (_ : nodoubles p l0) (_ : allex p l0 l1), permmod p l0 l1 *)
   intros m IH.
(* Goal: forall (p : nat) (l0 l1 l2 : Zlist) (_ : @eq nat (length Z l0) (S m)) (_ : @eq nat (length Z l1) (S m)) (_ : @eq nat (length Z l2) (S m)) (_ : permmod p l0 l1) (_ : permmod p l1 l2), permmod p l0 l2 *)
   intros p l0 l1 l2 Hl0 Hl1 Hl2 H01 H12.
(* Goal: permmod p l0 l1 *)
   apply allex_permmod. transitivity (length Z l1).
(* Goal: not (Mod a Z0 p) *)
   apply permmod_length with p. assumption.
(* Goal: not (Mod a Z0 p) *)
   apply permmod_length with p. assumption.
(* Goal: forall (x0 : Z) (_ : inlist Z x0 l0), @ex Z (fun x1 : Z => and (inlist Z x1 l2) (and (Mod x0 x1 p) (permmod p (zdrop x0 l0) (zdrop x1 l2)))) *)
   intros x0 Hx0.
(* Goal: @ex Z (fun x1 : Z => and (inlist Z x1 l2) (and (Mod x0 x1 p) (permmod p (zdrop x0 l0) (zdrop x1 l2)))) *)
   elim (permmod_allex p l0 l1 H01 x0). intros x1 H0.
(* Goal: @ex Z (fun x1 : Z => and (inlist Z x1 l2) (and (Mod x0 x1 p) (permmod p (zdrop x0 l0) (zdrop x1 l2)))) *)
(* Goal: inlist Z x0 l0 *)
   elim H0. intros Hx1 H1. elim H1. intros Hm01 Hd01.
(* Goal: @ex Z (fun x1 : Z => and (inlist Z x1 l2) (and (Mod x0 x1 p) (permmod p (zdrop x0 l0) (zdrop x1 l2)))) *)
(* Goal: inlist Z x0 l0 *)
   elim (permmod_allex p l1 l2 H12 x1). intros x2 H2.
(* Goal: @ex Z (fun x1 : Z => and (inlist Z x1 l2) (and (Mod x0 x1 p) (permmod p (zdrop x0 l0) (zdrop x1 l2)))) *)
(* Goal: inlist Z x1 l1 *)
(* Goal: inlist Z x0 l0 *)
   elim H2. intros Hx2 H3. elim H3. intros Hm12 Hd12.
(* Goal: @ex Z (fun x1 : Z => and (inlist Z x1 l2) (and (Mod x0 x1 p) (permmod p (zdrop x0 l0) (zdrop x1 l2)))) *)
(* Goal: inlist Z x1 l1 *)
(* Goal: inlist Z x0 l0 *)
   split with x2.
(* Goal: not (Mod a Z0 p) *)
   split. assumption.
(* Goal: not (Mod a Z0 p) *)
   split. apply mod_trans with x1. assumption. assumption.
(* Goal: permmod p (zdrop x0 l0) (zdrop x2 l2) *)
(* Goal: inlist Z x1 l1 *)
(* Goal: inlist Z x0 l0 *)
   apply IH with (zdrop x1 l1).
(* Goal: not (Mod a Z0 p) *)
   apply S_inj. rewrite zdrop_length. assumption. assumption.
(* Goal: not (Mod a Z0 p) *)
   apply S_inj. rewrite zdrop_length. assumption. assumption.
(* Goal: not (Mod a Z0 p) *)
   apply S_inj. rewrite zdrop_length. assumption. assumption.
(* Goal: not (Mod a Z0 p) *)
   assumption. assumption.
(* Goal: not (Mod a Z0 p) *)
   assumption. assumption.
Qed.

Lemma permmod_trans :
 forall (p : nat) (l0 l1 l2 : Zlist),
 permmod p l0 l1 -> permmod p l1 l2 -> permmod p l0 l2.
Proof.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros. apply permmod_trans1 with (length Z l0) l1.
(* Goal: @eq nat (length Z l0) (length Z l0) *)
(* Goal: @eq nat (length Z l0) (length Z l1) *)
(* Goal: Prime p *)
(* Goal: @eq nat (length Z l0) (length Z l1) *)
(* Goal: nodoubles p l0 *)
(* Goal: allex p l0 l1 *)
   reflexivity.
(* Goal: not (Mod a Z0 p) *)
   symmetry  in |- *. apply permmod_length with p. assumption.
(* Goal: @eq nat (length Z l0) (length Z l2) *)
(* Goal: permmod p l0 l1 *)
(* Goal: permmod p l1 l2 *)
   symmetry  in |- *. transitivity (length Z l1).
(* Goal: not (Mod a Z0 p) *)
   apply permmod_length with p. assumption.
(* Goal: not (Mod a Z0 p) *)
   apply permmod_length with p. assumption.
(* Goal: not (Mod a Z0 p) *)
   assumption. assumption.
Qed.

Lemma permmod_drop_drop1 :
 forall (n p : nat) (x y : Z) (l : Zlist),
 n = length Z l ->
 Mod x y p ->
 inlist Z x l -> inlist Z y l -> permmod p (zdrop x l) (zdrop y l).
Proof.
(* Goal: forall (n p : nat) (l0 l1 : Zlist) (_ : @eq nat n (length Z l0)) (_ : @eq nat n (length Z l1)) (_ : Prime p) (_ : @eq nat (length Z l0) (length Z l1)) (_ : nodoubles p l0) (_ : allex p l0 l1), permmod p l0 l1 *)
   simple induction n.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros. rewrite length_0 with Z l.
(* Goal: permmod p (zdrop x (Nil Z)) (zdrop y (Nil Z)) *)
(* Goal: @eq nat (length Z l) O *)
(* Goal: forall (n : nat) (_ : forall (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat n (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l)) (p : nat) (x y : Z) (l : Zlist) (_ : @eq nat (S n) (length Z l)) (_ : Mod x y p) (_ : inlist Z x l) (_ : inlist Z y l), permmod p (zdrop x l) (zdrop y l) *)
   simpl in |- *. reflexivity. symmetry  in |- *. assumption.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros m IH. intros.
(* Goal: permmod p (zdrop x l) (zdrop y l) *)
   elim (zeqdec x y).
(* Goal: not (@eq Z z y) *)
(* Goal: inlist Z z l *)
(* Goal: and (Mod z z p) (permmod p (zdrop z (zdrop x l)) (zdrop z (zdrop y l))) *)
   intro. rewrite H3. apply permmod_refl.
(* Goal: not (@eq Z z y) *)
(* Goal: inlist Z z l *)
(* Goal: and (Mod z z p) (permmod p (zdrop z (zdrop x l)) (zdrop z (zdrop y l))) *)
   intro. apply allex_permmod.
(* Goal: @eq nat (length Z (zdrop x l0)) (length Z (zdrop y l1)) *)
(* Goal: nodoubles p (zdrop x l0) *)
(* Goal: allex p (zdrop x l0) (zdrop y l1) *)
(* Goal: inlist Z x l0 *)
   apply S_inj.
(* Goal: @eq nat (length Z l0) (S (length Z (zdrop y l1))) *)
(* Goal: inlist Z x l0 *)
(* Goal: nodoubles p (zdrop x l0) *)
(* Goal: allex p (zdrop x l0) (zdrop y l1) *)
(* Goal: inlist Z x l0 *)
   rewrite zdrop_length. rewrite zdrop_length.
(* Goal: not (Mod a Z0 p) *)
   reflexivity. assumption. assumption.   
(* Goal: forall (x0 : Z) (_ : inlist Z x0 (zdrop x l)), @ex Z (fun x1 : Z => and (inlist Z x1 (zdrop y l)) (and (Mod x0 x1 p) (permmod p (zdrop x0 (zdrop x l)) (zdrop x1 (zdrop y l))))) *)
   intros z Hz.
(* Goal: @ex Z (fun x1 : Z => and (inlist Z x1 (zdrop y l)) (and (Mod z x1 p) (permmod p (zdrop z (zdrop x l)) (zdrop x1 (zdrop y l))))) *)
   elim (zeqdec y z).
(* Goal: not (@eq Z z y) *)
(* Goal: inlist Z z l *)
(* Goal: and (Mod z z p) (permmod p (zdrop z (zdrop x l)) (zdrop z (zdrop y l))) *)
   intro. split with x.
(* Goal: not (Mod a Z0 p) *)
   split. apply zdrop_neq_inlist. assumption. assumption.
(* Goal: not (Mod a Z0 p) *)
   split. rewrite <- H4. apply mod_sym. assumption.
(* Goal: permmod p (zdrop z (zdrop x l)) (zdrop x (zdrop z l)) *)
(* Goal: forall _ : not (@eq Z y z), @ex Z (fun x1 : Z => and (inlist Z x1 (zdrop y l)) (and (Mod z x1 p) (permmod p (zdrop z (zdrop x l)) (zdrop x1 (zdrop y l))))) *)
   rewrite H4. rewrite zdrop_swap. apply permmod_refl.
(* Goal: not (@eq Z z y) *)
(* Goal: inlist Z z l *)
(* Goal: and (Mod z z p) (permmod p (zdrop z (zdrop x l)) (zdrop z (zdrop y l))) *)
   intro. split with z.
(* Goal: and (Mod x y p) (permmod p (zdrop x l0) (zdrop y l1)) *)
(* Goal: inlist Z x l0 *)
   split. apply zdrop_neq_inlist.
(* Goal: not (Mod a Z0 p) *)
   intro. apply H4. symmetry  in |- *. assumption.
(* Goal: inlist Z z l *)
(* Goal: Mod x y p *)
(* Goal: inlist Z x (zdrop z l) *)
(* Goal: inlist Z y (zdrop z l) *)
   apply zdrop_inlist_weak with x. assumption.
(* Goal: and (Mod x y p) (permmod p (zdrop x l0) (zdrop y l1)) *)
(* Goal: inlist Z x l0 *)
   split. apply mod_refl.
(* Goal: permmod p (zdrop x (zdrop z l)) (zdrop z (zdrop y l)) *)
   rewrite (zdrop_swap z). rewrite (zdrop_swap z).
(* Goal: permmod p (zdrop x (zdrop z l)) (zdrop y (zdrop z l)) *)
   apply (IH p x y (zdrop z l)).
(* Goal: not (Mod a Z0 p) *)
   apply S_inj. rewrite zdrop_length. assumption.
(* Goal: inlist Z z l *)
(* Goal: Mod x y p *)
(* Goal: inlist Z x (zdrop z l) *)
(* Goal: inlist Z y (zdrop z l) *)
   apply zdrop_inlist_weak with x. assumption.
(* Goal: not (Mod a Z0 p) *)
   assumption.
(* Goal: not (Mod a Z0 p) *)
   apply zdrop_inlist_swap. assumption. assumption.
(* Goal: not (Mod a Z0 p) *)
   apply zdrop_neq_inlist. assumption. assumption.
Qed.

Lemma permmod_drop_drop :
 forall (p : nat) (x y : Z) (l : Zlist),
 Mod x y p ->
 inlist Z x l -> inlist Z y l -> permmod p (zdrop x l) (zdrop y l).
Proof.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros. apply permmod_drop_drop1 with (length Z l).
(* Goal: not (Mod a Z0 p) *)
   reflexivity. assumption. assumption. assumption.
Qed.

Lemma permmod_drop_rev :
 forall (p : nat) (l0 l1 : Zlist) (x0 x1 : Z),
 Mod x0 x1 p ->
 inlist Z x0 l0 ->
 inlist Z x1 l1 -> permmod p l0 l1 -> permmod p (zdrop x0 l0) (zdrop x1 l1).
Proof.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros. elim (permmod_allex p l0 l1 H2 x0).
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros y Hy. elim Hy. intros. elim H4. intros.
(* Goal: not (Mod a Z0 p) *)
   apply permmod_trans with (zdrop y l1). assumption.
(* Goal: permmod p (zdrop y l1) (zdrop x1 l1) *)
(* Goal: inlist Z x0 l0 *)
   apply permmod_drop_drop.
(* Goal: not (Mod a Z0 p) *)
   apply mod_trans with x0. apply mod_sym. assumption.
(* Goal: not (Mod a Z0 p) *)
   assumption. assumption. assumption. assumption.
Qed.

Lemma nodoubles_allex_permmod1 :
 forall (n p : nat) (l0 l1 : Zlist),
 n = length Z l0 ->
 n = length Z l1 ->
 Prime p ->
 length Z l0 = length Z l1 ->
 nodoubles p l0 -> allex p l0 l1 -> permmod p l0 l1.
Proof.
(* Goal: forall (n p : nat) (l0 l1 : Zlist) (_ : @eq nat n (length Z l0)) (_ : @eq nat n (length Z l1)) (_ : Prime p) (_ : @eq nat (length Z l0) (length Z l1)) (_ : nodoubles p l0) (_ : allex p l0 l1), permmod p l0 l1 *)
   simple induction n.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros.
(* Goal: permmod p l0 l1 *)
(* Goal: forall (n : nat) (_ : forall (p : nat) (l0 l1 : Zlist) (_ : @eq nat n (length Z l0)) (_ : @eq nat n (length Z l1)) (_ : Prime p) (_ : @eq nat (length Z l0) (length Z l1)) (_ : nodoubles p l0) (_ : allex p l0 l1), permmod p l0 l1) (p : nat) (l0 l1 : Zlist) (_ : @eq nat (S n) (length Z l0)) (_ : @eq nat (S n) (length Z l1)) (_ : Prime p) (_ : @eq nat (length Z l0) (length Z l1)) (_ : nodoubles p l0) (_ : allex p l0 l1), permmod p l0 l1 *)
   rewrite length_0 with Z l0.
(* Goal: permmod p (Nil Z) l1 *)
(* Goal: @eq nat (length Z l0) O *)
(* Goal: forall (n : nat) (_ : forall (p : nat) (l0 l1 : Zlist) (_ : @eq nat n (length Z l0)) (_ : @eq nat n (length Z l1)) (_ : Prime p) (_ : @eq nat (length Z l0) (length Z l1)) (_ : nodoubles p l0) (_ : allex p l0 l1), permmod p l0 l1) (p : nat) (l0 l1 : Zlist) (_ : @eq nat (S n) (length Z l0)) (_ : @eq nat (S n) (length Z l1)) (_ : Prime p) (_ : @eq nat (length Z l0) (length Z l1)) (_ : nodoubles p l0) (_ : allex p l0 l1), permmod p l0 l1 *)
   rewrite length_0 with Z l1. 
(* Goal: permmod p (Nil Z) (Nil Z) *)
(* Goal: @eq nat (length Z l1) O *)
(* Goal: @eq nat (length Z l0) O *)
(* Goal: forall (n : nat) (_ : forall (p : nat) (l0 l1 : Zlist) (_ : @eq nat n (length Z l0)) (_ : @eq nat n (length Z l1)) (_ : Prime p) (_ : @eq nat (length Z l0) (length Z l1)) (_ : nodoubles p l0) (_ : allex p l0 l1), permmod p l0 l1) (p : nat) (l0 l1 : Zlist) (_ : @eq nat (S n) (length Z l0)) (_ : @eq nat (S n) (length Z l1)) (_ : Prime p) (_ : @eq nat (length Z l0) (length Z l1)) (_ : nodoubles p l0) (_ : allex p l0 l1), permmod p l0 l1 *)
   apply permmod_nil.
(* Goal: not (Mod a Z0 p) *)
   symmetry  in |- *. assumption. symmetry  in |- *. assumption.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros m IH. intros.
(* Goal: permmod p l0 l1 *)
   apply allex_permmod.
(* Goal: not (Mod a Z0 p) *)
   assumption.
(* Goal: forall (x0 : Z) (_ : inlist Z x0 l0), @ex Z (fun x1 : Z => and (inlist Z x1 l1) (and (Mod x0 x1 p) (permmod p (zdrop x0 l0) (zdrop x1 l1)))) *)
   intros x Hx. elim H4 with x.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros y Hy. elim Hy. intros.
(* Goal: @ex Z (fun x1 : Z => and (inlist Z x1 l1) (and (Mod x x1 p) (permmod p (zdrop x l0) (zdrop x1 l1)))) *)
(* Goal: inlist Z x l0 *)
   split with y.
(* Goal: not (Mod a Z0 p) *)
   split. assumption.
(* Goal: not (Mod a Z0 p) *)
   split. assumption.
(* Goal: permmod p (zdrop x l0) (zdrop y l1) *)
(* Goal: inlist Z x l0 *)
   apply IH.
(* Goal: not (Mod a Z0 p) *)
   apply S_inj. rewrite zdrop_length. assumption.
(* Goal: not (Mod a Z0 p) *)
   assumption.
(* Goal: not (Mod a Z0 p) *)
   apply S_inj. rewrite zdrop_length. assumption.
(* Goal: not (Mod a Z0 p) *)
   assumption.
(* Goal: not (Mod a Z0 p) *)
   assumption.
(* Goal: @eq nat (length Z (zdrop x l0)) (length Z (zdrop y l1)) *)
(* Goal: nodoubles p (zdrop x l0) *)
(* Goal: allex p (zdrop x l0) (zdrop y l1) *)
(* Goal: inlist Z x l0 *)
   apply S_inj. rewrite zdrop_length.
(* Goal: not (Mod a Z0 p) *)
   rewrite zdrop_length. assumption.
(* Goal: not (Mod a Z0 p) *)
   assumption. assumption.
(* Goal: not (Mod a Z0 p) *)
   apply nodoubles_drop. assumption.
(* Goal: allex p (zdrop x l0) (zdrop y l1) *)
(* Goal: inlist Z x l0 *)
   apply allex_nodoubles_drop.
(* Goal: not (Mod a Z0 p) *)
   assumption. assumption. assumption. assumption.
(* Goal: not (Mod a Z0 p) *)
   assumption. assumption. assumption.
Qed.

Lemma nodoubles_allex_permmod :
 forall (p : nat) (l0 l1 : Zlist),
 Prime p ->
 length Z l0 = length Z l1 ->
 nodoubles p l0 -> allex p l0 l1 -> permmod p l0 l1.
Proof.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros. apply nodoubles_allex_permmod1 with (length Z l0).
(* Goal: not (Mod a Z0 p) *)
   reflexivity. assumption. assumption. assumption.
(* Goal: not (Mod a Z0 p) *)
   assumption. assumption.
Qed.

Lemma until_mapmult_permmod :
 forall (p : nat) (a : Z),
 Prime p ->
 ~ Mod a 0 p -> permmod p (until (pred p)) (mapmult a (until (pred p))).
Proof.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros.
(* Goal: permmod p (until (Init.Nat.pred p)) (mapmult a (until (Init.Nat.pred p))) *)
   apply nodoubles_allex_permmod.
(* Goal: not (Mod a Z0 p) *)
   assumption. unfold mapmult in |- *. apply map_length.
(* Goal: not (Mod a Z0 p) *)
   apply until_nodoubles. assumption.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   unfold allex in |- *. intros.
(* Goal: @ex Z (fun y : Z => and (inlist Z y (mapmult a (until (Init.Nat.pred p)))) (Mod x y p)) *)
   apply (until_mapmult_allex p a H H0).
(* Goal: not (Mod a Z0 p) *)
   assumption.
Qed.

(** * Fermat's Little Theorem. *)

Theorem flt :
 forall (a : Z) (p : nat), Prime p -> ~ Mod a 0 p -> Mod (Exp a (pred p)) 1 p.
Proof.
(* Goal: forall (a : Z) (p : nat) (_ : Prime p) (_ : not (Mod a Z0 p)), Mod (Exp a (Init.Nat.pred p)) (Zpos xH) p *)
   intros. apply mod_sym.
(* Goal: Mod (Zpos xH) (Exp a (Init.Nat.pred p)) p *)
   apply mod_mult_cancel_r with (zproduct (until (pred p))).
(* Goal: not (Mod a Z0 p) *)
   assumption. apply until_prod_not_0mod. assumption.
(* Goal: Mod (Z.mul (Zpos xH) (zproduct (until (Init.Nat.pred p)))) (Z.mul (Exp a (Init.Nat.pred p)) (zproduct (until (Init.Nat.pred p)))) p *)
   rewrite <- until_mapmult_exp. rewrite Zmult_1_l.
(* Goal: Mod (zproduct (until (Init.Nat.pred p))) (zproduct (mapmult a (until (Init.Nat.pred p)))) p *)
   apply permmod_product. apply until_mapmult_permmod.
(* Goal: not (Mod a Z0 p) *)
   assumption. assumption.
Qed.
