(**
 * fermat.
 * Fermat's little theorem.
 *
 * @author Martijn Oostdijk
 * @version $Revision$
 *)

Require Arith.
Require ZArith.

Require lemmas.
Require natZ.
Require dec.
Require list.
Require exp.
Require divides.
Require prime.
Require mod.
Require modprime.

(* No double elements modulo p. *)

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

Lemma nodoubles_nil:
   (p:nat)(nodoubles p (Nil Z)).
Proof.
   Unfold nodoubles. Simpl. Intros. Elim H0.
Qed.

Lemma nodoubles_drop:
   (p:nat)(l:Zlist)(x:Z)
      (nodoubles p l)->(nodoubles p (zdrop x l)).
Proof.
   Unfold nodoubles. Intros. Apply H.
   Apply zdrop_inlist_weak with x. Assumption.
   Apply zdrop_inlist_weak with x. Rewrite zdrop_swap. Assumption.
Qed.

Lemma nodoubles_ind:
   (p:nat)
      (h:Z)(t:Zlist)
         ((x:Z)(inlist Z x t)->~(Mod h x p))->
            (nodoubles p t)->
               (nodoubles p (Cons Z h t)).
Proof.
   Intros. Unfold nodoubles. Intros.
   Elim (zeqdec x h).
   Intro. Rewrite zdrop_head_eq in H2.
   Rewrite H3. Apply (H y). Assumption. Assumption.
   Intro. Rewrite zdrop_head_neq in H2.
   Elim (zeqdec y h).
   Intro. Rewrite H4. Intro. Elim (H x).
   Elim (inlist_head_neq Z x h t). Intros.
   Apply H6. Assumption. Assumption.
   Apply mod_sym. Assumption.
   Intro. Unfold nodoubles in H0.
   Apply (H0 x).
   Elim (inlist_head_neq Z x h t). Intros.
   Apply H5. Assumption. Assumption.
   Elim (inlist_head_neq Z y h (zdrop x t)). Intros.
   Apply H5. Assumption. Assumption.
   Assumption.
Qed.

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

Definition allex [p:nat; l0,l1:Zlist]: Prop :=
   (x:Z)(inlist Z x l0)->(EX y:Z | (inlist Z y l1) /\ (Mod x y p)).

Lemma allex_nodoubles_drop:
      (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.
   Intros.
   Unfold allex. Intros x Hx.
   Elim (H4 x). Intros y Hy.
   Elim Hy. Intros.
   Split with y.
   Split. Apply zdrop_neq_inlist.
   Intro. Rewrite H7 in H6.
   Elim H3 with x x0.
   Apply zdrop_inlist_weak with x0. Assumption.
   Apply zdrop_inlist_swap. Assumption. Assumption.
   Apply mod_trans with x1. Assumption.
   Apply mod_sym. Assumption.
   Assumption. Assumption.
   Apply zdrop_inlist_weak with x0. Assumption.
Qed.

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

Fixpoint until[n:nat]: Zlist := 
   Cases n of
      O     => (Nil Z)
    | (S n) => (Cons Z (inject_nat (S n)) (until n))
   end.

Lemma until_ok: (n:nat)(x:Z)`0<x<=(inject_nat n)`->(inlist Z x (until n)).
Proof.
   Induction n.
   Simpl. Intros. Elim H. Intros.
   Elim (Zle_not_lt x `0`). Assumption. Assumption.
   Intros m IH. Intros. Elim H. Intros.
   Elim (Zle_lt_or_eq x (inject_nat (S m))).
   Intros. Unfold inlist. Simpl. Right. Unfold inlist in IH.
   Apply IH. Split. Assumption.
   Apply Zlt_n_Sm_le. Rewrite <- inj_S. Assumption.
   Intro. Rewrite H2. Unfold inlist.
   Simpl. Left. Reflexivity. Assumption.
Qed.

Lemma until_mod_all:
   (p:nat; x:Z)
      (lt O p)->~(Mod x `0` p)->
         (EX y:Z | (inlist Z y (until (pred p)))/\(Mod x y p)).
Proof.
   Intros.
   Elim (zdiv_rem (inject_nat p) x).
   Intro q. Intros.
   Elim H1. Intro r. Intros.
   Elim H2. Intros. Elim H3. Intros.
   Elim (Zle_lt_or_eq `0` r).

   (* case 0 < r *)
   Intro. Split with r. Split.
   Apply until_ok. Split.
   Assumption.
   Apply Zlt_n_Sm_le. Rewrite <- inj_S. Rewrite <- (S_pred p O).
   Assumption. Assumption.
   Split with q. Rewrite Zplus_sym. Rewrite Zmult_sym. Assumption.

   (* case 0 = r *)
   Intro. Elim H0. Split with q.
   Rewrite H7. Rewrite Zplus_sym. Rewrite Zmult_sym. Assumption.

   Assumption.
   Change `(inject_nat p) > (inject_nat O)`. Apply inj_gt. Assumption.
Qed.

Lemma until_pos:
   (n:nat; x:Z)(inlist Z x (until n))->`0 < x`.
Proof.
   Induction n.
   Unfold inlist. Simpl. Intros. Elim H.
   Intros m IH. Intros. Unfold inlist in H. Simpl in H. Elim H. Intros.
   Rewrite H0. Unfold Zlt. Simpl. Reflexivity.
   Intros. Apply IH. Assumption.
Qed.

Lemma until_le_n:
   (n:nat; x:Z)(inlist Z x (until n))->`x <= (inject_nat n)`.
Proof.
   Induction n.
   Unfold inlist. Simpl. Intros. Elim H.
   Intros m IH. Intros. Unfold inlist in H. Simpl in H. Elim H. Intros.
   Rewrite H0. Apply Zle_n.
   Intros. Apply Zle_trans with (inject_nat m).
   Apply IH. Assumption. Apply inj_le. Apply le_S. Apply le_n.
Qed.

Lemma until_not_0mod:
   (p:nat; x:Z)(lt O p)->(inlist Z x (until (pred p)))->~(Mod x `0` p).
Proof.
   Intros. Apply mod_repr_non_0. Split.
   Apply (until_pos (pred p) x). Assumption.
   Rewrite (S_pred p O). Rewrite inj_S.
   Apply Zle_lt_n_Sm. Apply until_le_n.
   Assumption. Assumption.
Qed.

Lemma untiln_prod_not_0modp:
   (p:nat)(n:nat)
      (lt O n)->(lt n p)->(Prime p)->~(Mod (zproduct (until n)) `0` p).
Proof.
   Induction n.
   Intro. Elim (lt_n_n O). Assumption.
   Intros m IH H0m Hmp Hp.
   Change ~(Mod `(inject_nat (S m))*(zproduct (until m))` `0` p).
   Intro. Elim (mod_mult_0 p (inject_nat (S m)) (zproduct (until m))).
   Intro. Elim (mod_repr_non_0 p (inject_nat (S m))). Split.
   Change `(inject_nat O) < (inject_nat (S m))`.
   Apply inj_lt. Assumption.
   Apply inj_lt. Assumption.
   Assumption.
   Intro. Elim (le_lt_or_eq O m). Intro.
   Elim IH. Assumption. Apply lt_trans with (S m).
   Apply lt_n_Sn. Assumption. Assumption.
   Assumption. Intro. Rewrite <- H1 in H. Simpl in H.
   Elim mod_0not1 with p. Elim Hp. Intros. Assumption.
   Apply mod_sym. Assumption.
   Apply le_O_n. Assumption.
   Assumption.
Qed.

Lemma until_prod_not_0mod:
   (p:nat)(Prime p)->~(Mod (zproduct (until (pred p))) `0` p).
Proof.
   Intros. Elim H. Intros.
   Apply untiln_prod_not_0modp;
   Auto with arith.
Qed.

Lemma until_mapmult_exp:
   (a:Z)(n:nat)
      (zproduct (mapmult a (until n))) = `(Exp a n)*(zproduct (until n))`.
Proof.
   Induction n.
   Simpl. Reflexivity.
   Intros m IH.
   Replace (mapmult a (until (S m)))
      with (Cons Z `a*(inject_nat (S m))` (mapmult a (until m))).
   Rewrite exp_S.
   Replace `(zproduct (Cons Z (a*(inject_nat (S m))) (mapmult a (until m))))`
      with `(a*(inject_nat (S m)))*(zproduct (mapmult a (until m)))`.
   Rewrite IH. Rewrite Zmult_assoc_r.
   Rewrite (Zmult_assoc_l (inject_nat (S m)) (Exp a m)).
   Rewrite (Zmult_sym (inject_nat (S m))).
   Rewrite Zmult_assoc_l. Rewrite Zmult_assoc_l.
   Replace (zproduct (until (S m)))
      with `(inject_nat (S m))*(zproduct (until m))`.
   Rewrite Zmult_assoc_l. Reflexivity.
   Reflexivity. Reflexivity. Reflexivity.
Qed.

Lemma until_mapmult_allex:
   (p:nat)(a:Z)
      (Prime p)->~(Mod a `0` p)->
         (allex p (until (pred p)) (mapmult a (until (pred p)))).
Proof.
   Unfold allex.
   Intros p a Hprime Ha0 x Hx. Elim Hprime. Intros Hp Hp1.
   Elim (mod_mult_inv_r a p). Intros ra Hra.
   Elim (zdiv_rem (inject_nat p) `ra*x`). Intros q Hq. Elim Hq.
   Intros r Hr. Elim Hr. Intros. Elim H. Intros.
   Split with `a*r`.
   Split. Apply mapmult_image. Apply until_ok.
   Split. Elim (Zle_lt_or_eq `0` r). Intro. Assumption.
   Intro. Rewrite <- H3 in H0. Rewrite <- Zplus_n_O in H0.
   Elim until_not_0mod with p x.
   Apply lt_trans with (1). Apply lt_n_Sn. Assumption.
   Assumption.
   Apply mod_mult_cancel_r with `a*ra`. Assumption.
   Intro. Elim mod_0not1 with p. Assumption.
   Apply mod_trans with `a*ra`. Apply mod_sym. Assumption. Assumption.
   Rewrite (Zmult_sym a ra). Rewrite Zmult_assoc_l. Rewrite (Zmult_sym x ra).
   Rewrite H0. Simpl. Unfold Mod. Split with `q*a`. Simpl.
   Rewrite Zmult_assoc_l. Rewrite (Zmult_sym q). Reflexivity.
   Assumption. Apply Zlt_n_Sm_le.
   Rewrite <- inj_S. Rewrite <- (S_pred p (1)). Assumption.
   Assumption.
   Apply mod_mult_cancel_r with ra. Assumption.
   Intro. Elim mod_0not1 with p. Assumption.
   Apply mod_trans with `ra*a`. Change (Mod `0*a` `ra*a` p).
   Apply mod_mult_compat. Apply mod_sym. Assumption.
   Apply mod_refl. Rewrite (Zmult_sym ra a). Assumption.
   Rewrite (Zmult_sym x ra). Rewrite H0.
   Rewrite (Zmult_sym a r). Rewrite (Zmult_assoc_r r a ra).
   Apply mod_trans with r. Split with q.
   Rewrite Zplus_sym. Rewrite Zmult_sym. Reflexivity.
   Pattern 1 r. Rewrite <- Zmult_one with r.
   Rewrite (Zmult_sym `1` r). Apply mod_mult_compat.
   Apply mod_refl. Apply mod_sym. Assumption.
   Change `(inject_nat p) > (inject_nat O)`. Apply inj_gt.
   Apply gt_trans with (1). Assumption. Apply gt_Sn_n.
   Assumption. Assumption.
Qed.

Lemma until_nodoubles1:
   (p:nat)(Prime p)->(n:nat)(lt n p)->(nodoubles p (until n)).
Proof.
   Induction n.
   Intros. Simpl. Apply nodoubles_nil.
   Intros m IH Hb.
   Change (nodoubles p (Cons Z (inject_nat (S m)) (until m))).
   Apply nodoubles_ind. Intros.
   Intro. Elim (Zlt_not_le x (inject_nat (S m))).
   Rewrite inj_S. Apply Zle_lt_n_Sm. Apply until_le_n.
   Assumption. Apply Zle_refl. Apply mod_repr_eq with p.
   Elim H. Intros. Apply lt_trans with (1). Apply lt_n_Sn. Assumption.
   Split. Change `(inject_nat O) < (inject_nat (S m))`. Apply inj_lt.
   Apply lt_O_Sn. Apply inj_lt. Assumption.
   Split. Apply until_pos with m. Assumption.
   Apply Zle_lt_trans with (inject_nat m).
   Apply until_le_n. Assumption.
   Apply inj_lt. Apply le_lt_trans with (S m).
   Apply le_n_Sn. Assumption.
   Assumption.
   Apply IH. Apply le_lt_trans with (S m).
   Apply le_n_Sn. Assumption.
Qed.

Lemma until_nodoubles:
   (p:nat)(Prime p)->(nodoubles p (until (pred p))).
Proof.
   Intros. Apply until_nodoubles1. Assumption.
   Apply lt_pred_n_n. Apply lt_trans with (1).
   Apply lt_n_Sn. Elim H. Intros. Assumption.
Qed.

(* Permutations modulo p. *)

Fixpoint permmod [p:nat; l1:Zlist]: Zlist -> Prop :=
   [l2:Zlist]
   Cases l1 of
      Nil        => l2=(Nil Z)
    | (Cons x t) => (EX y:Z | (inlist Z y l2) /\
                       (Mod x y p) /\ (permmod p t (zdrop y l2)))
   end.

Lemma permmod_nil:
   (p:nat)(permmod p (Nil Z) (Nil Z)).
Proof.
   Simpl. Intro. Reflexivity.
Qed.

Lemma permmod_drop:
   (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.
   Induction l1.
   Simpl. Intros. Elim H0.
   Intros h t IH. Intros l2 Hm.
   Elim (zeqdec x1 h).
   Intros. Simpl. Split with x2.
   Split. Assumption.
   Split. Rewrite <- H. Assumption.
   Rewrite H in H2. Rewrite zdrop_head_eq in H2.
   Assumption. Reflexivity.
   Intro.
   Rewrite zdrop_head_neq.
   Intros. Elim H2. Intros y Hy.
   Elim Hy. Intros. Elim H4. Intros.
   Split with y. Split.
   Apply zdrop_inlist_weak with x2. Assumption.
   Split. Assumption.
   Rewrite zdrop_swap in H6.
   Apply IH. Assumption.
   Elim (inlist_head_neq Z x1 h t). Intros. Apply H7. Assumption.
   Assumption.
   Elim (zeqdec x2 y).
   Intro. Rewrite H7. Rewrite H7 in H3. Assumption.
   Intro. Apply zdrop_neq_inlist. Assumption. Assumption.
   Assumption. Assumption.
Qed.

Lemma permmod_drop_cons:
   (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.
   Intros. Apply permmod_drop with x1 x2.
   Assumption.
   Apply inlist_head_eq. Reflexivity.
   Assumption.
   Rewrite zdrop_head_eq. Assumption.
   Reflexivity.
Qed.

Lemma permmod_cons_extend:
   (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.
   Intros.
   Apply permmod_drop with x1 x2.
   Assumption.
   Apply inlist_head_eq. Reflexivity.
   Apply inlist_head_eq. Reflexivity.
   Rewrite zdrop_head_eq. Rewrite zdrop_head_eq.
   Assumption. Reflexivity. Reflexivity.
Qed.

Lemma permmod_length:
   (p:nat)(l1,l2:Zlist)(permmod p l1 l2)->
      (length Z l1)=(length Z l2).
Proof.
   Induction l1.
   Simpl. Intros. Rewrite H. Simpl. Reflexivity.
   Intros h t IH. Simpl. Intros.
   Elim H. Intros y Hy.  Elim Hy. Intros.
   Elim H1. Intros.
   Rewrite (IH (zdrop y l2)).
   Rewrite zdrop_length with y l2.
   Reflexivity. Assumption. Assumption.
Qed.

Lemma permmod_refl:
   (p:nat)(l:Zlist)(permmod p l l).
Proof.
   Induction l.
   Simpl. Reflexivity.
   Intros h t IH. Split with h.
   Split. Apply inlist_head_eq. Reflexivity.
   Split. Apply mod_refl.
   Rewrite zdrop_head_eq. Assumption. Reflexivity.
Qed.

Lemma permmod_sym:
   (p:nat)(l1,l2:Zlist)
      (permmod p l1 l2)->(permmod p l2 l1).
Proof.
   Induction l1.
   Simpl. Intros. Rewrite H. Apply permmod_nil.
   Intros h1 t1 IH1.
   Intros. Elim H. Intros y Hy.
   Elim Hy. Intros. Elim H1. Intros.
   Apply permmod_drop with y h1.
   Apply mod_sym. Assumption.
   Assumption.
   Apply inlist_head_eq. Reflexivity.
   Rewrite zdrop_head_eq. Apply IH1.
   Assumption.
   Reflexivity.
Qed.

Lemma permmod_product:
   (l0,l1:Zlist)(p:nat)
      (permmod p l0 l1)->(Mod (zproduct l0) (zproduct l1) p).
Proof.
   Induction l0.
   Simpl. Intros. Rewrite H. Simpl. Apply mod_refl.
   Intros h t IH. Intros.
   Elim H. Intros. Elim H0. Intros. Elim H2. Intros.
   Simpl. Rewrite <- zdrop_product with x l1.
   Apply mod_mult_compat.
   Assumption.
   Apply IH. Assumption.
   Assumption.
Qed.

Lemma allex_permmod:
   (p:nat)(l0,l1:Zlist)
      (length Z l0)=(length Z l1)->
      ((x0:Z)(inlist Z x0 l0)->
         (EX x1:Z | (inlist Z x1 l1)/\
                    (Mod x0 x1 p)/\
                    (permmod p (zdrop x0 l0) (zdrop x1 l1))))->
            (permmod p l0 l1).
Proof.
   Induction l0.
   Induction l1.
   Intros. Apply permmod_nil.
   Intros. Discriminate H0.
   Intros h0 t0 IH0. Intros.
   Elim (H0 h0). Intro x1. Intros.
   Elim H1. Intros. Elim H3. Intros.
   Rewrite zdrop_head_eq in H5.
   Apply permmod_drop_cons with x1.
   Assumption. Assumption. Assumption.
   Reflexivity.
   Apply inlist_head_eq. Reflexivity.
Qed.

Lemma permmod_allex:
   (p:nat)(l0,l1:Zlist)
      (permmod p l0 l1)->
         (x:Z)(inlist Z x l0)->
            (EX y:Z | (inlist Z y l1) /\ (Mod x y p) /\
               (permmod p (zdrop x l0) (zdrop y l1))).
Proof.
   Induction l0.
   Intros. Elim H0.
   Intros h0 t0 IH0. Intros.
   Elim H. Intros h1 Hh1.
   Elim Hh1. Intros. Elim H2. Intros.
   Elim (zeqdec x h0).
   Intro. Split with h1.
   Split. Assumption.
   Split. Rewrite H5. Assumption.
   Rewrite zdrop_head_eq. Assumption. Assumption.
   Intro. Elim (IH0 (zdrop h1 l1) H4 x).
   Intros y Hy. Elim Hy. Intros. Elim H7. Intros.
   Split with y.
   Split. Apply zdrop_inlist_weak with h1. Assumption.
   Split. Assumption.
   Rewrite zdrop_head_neq. Split with h1.
   Split. Elim (zeqdec h1 y).
   Intro. Rewrite H10 in H6. Rewrite H10. Assumption.
   Intro. Apply zdrop_neq_inlist. Assumption. Assumption.
   Split. Assumption. Rewrite zdrop_swap. Assumption.
   Assumption. Elim (inlist_head_neq Z x h0 t0).
   Intros. Apply H6. Assumption. Assumption.
Qed.

Lemma permmod_trans1:
   (n:nat)(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.
   Induction n.
   Intros.
   Rewrite length_0 with Z l0.
   Rewrite length_0 with Z l2.
   Apply permmod_nil. Assumption. Assumption.
   Intros m IH.
   Intros p l0 l1 l2 Hl0 Hl1 Hl2 H01 H12.
   Apply allex_permmod. Transitivity (length Z l1).
   Apply permmod_length with p. Assumption.
   Apply permmod_length with p. Assumption.
   Intros x0 Hx0.
   Elim (permmod_allex p l0 l1 H01 x0). Intros x1 H0.
   Elim H0. Intros Hx1 H1. Elim H1. Intros Hm01 Hd01.
   Elim (permmod_allex p l1 l2 H12 x1). Intros x2 H2.
   Elim H2. Intros Hx2 H3. Elim H3. Intros Hm12 Hd12.
   Split with x2.
   Split. Assumption.
   Split. Apply mod_trans with x1. Assumption. Assumption.
   Apply IH with (zdrop x1 l1).
   Apply S_inj. Rewrite zdrop_length. Assumption. Assumption.
   Apply S_inj. Rewrite zdrop_length. Assumption. Assumption.
   Apply S_inj. Rewrite zdrop_length. Assumption. Assumption.
   Assumption. Assumption.
   Assumption. Assumption.
Qed.

Lemma permmod_trans:
   (p:nat)(l0,l1,l2:Zlist)
         (permmod p l0 l1)->(permmod p l1 l2)->(permmod p l0 l2).
Proof.
   Intros. Apply permmod_trans1 with (length Z l0) l1.
   Reflexivity.
   Symmetry. Apply permmod_length with p. Assumption.
   Symmetry. Transitivity (length Z l1).
   Apply permmod_length with p. Assumption.
   Apply permmod_length with p. Assumption.
   Assumption. Assumption.
Qed.

Lemma permmod_drop_drop1:
   (n:nat)(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.
   Induction n.
   Intros. Rewrite length_0 with Z l.
   Simpl. Reflexivity. Symmetry. Assumption.
   Intros m IH. Intros.
   Elim (zeqdec x y).
   Intro. Rewrite H3. Apply permmod_refl.
   Intro. Apply allex_permmod.
   Apply S_inj.
   Rewrite zdrop_length. Rewrite zdrop_length.
   Reflexivity. Assumption. Assumption.   
   Intros z Hz.
   Elim (zeqdec y z).
   Intro. Split with x.
   Split. Apply zdrop_neq_inlist. Assumption. Assumption.
   Split. Rewrite <- H4. Apply mod_sym. Assumption.
   Rewrite H4. Rewrite zdrop_swap. Apply permmod_refl.
   Intro. Split with z.
   Split. Apply zdrop_neq_inlist.
   Intro. Apply H4. Symmetry. Assumption.
   Apply zdrop_inlist_weak with x. Assumption.
   Split. Apply mod_refl.
   Rewrite (zdrop_swap z). Rewrite (zdrop_swap z).
   Apply (IH p x y (zdrop z l)).
   Apply S_inj. Rewrite zdrop_length. Assumption.
   Apply zdrop_inlist_weak with x. Assumption.
   Assumption.
   Apply zdrop_inlist_swap. Assumption. Assumption.
   Apply zdrop_neq_inlist. Assumption. Assumption.
Qed.

Lemma permmod_drop_drop:
   (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.
   Intros. Apply permmod_drop_drop1 with (length Z l).
   Reflexivity. Assumption. Assumption. Assumption.
Qed.

Lemma permmod_drop_rev:
   (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.
   Intros. Elim (permmod_allex p l0 l1 H2 x0).
   Intros y Hy. Elim Hy. Intros. Elim H4. Intros.
   Apply permmod_trans with (zdrop y l1). Assumption.
   Apply permmod_drop_drop.
   Apply mod_trans with x0. Apply mod_sym. Assumption.
   Assumption. Assumption. Assumption. Assumption.
Qed.

Lemma nodoubles_allex_permmod1:
   (n:nat)
      (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.
   Induction n.
   Intros.
   Rewrite length_0 with Z l0.
   Rewrite length_0 with Z l1. 
   Apply permmod_nil.
   Symmetry. Assumption. Symmetry. Assumption.
   Intros m IH. Intros.
   Apply allex_permmod.
   Assumption.
   Intros x Hx. Elim H4 with x.
   Intros y Hy. Elim Hy. Intros.
   Split with y.
   Split. Assumption.
   Split. Assumption.
   Apply IH.
   Apply S_inj. Rewrite zdrop_length. Assumption.
   Assumption.
   Apply S_inj. Rewrite zdrop_length. Assumption.
   Assumption.
   Assumption.
   Apply S_inj. Rewrite zdrop_length.
   Rewrite zdrop_length. Assumption.
   Assumption. Assumption.
   Apply nodoubles_drop. Assumption.
   Apply allex_nodoubles_drop.
   Assumption. Assumption. Assumption. Assumption.
   Assumption. Assumption. Assumption.
Qed.

Lemma nodoubles_allex_permmod:
   (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.
   Intros. Apply nodoubles_allex_permmod1 with (length Z l0).
   Reflexivity. Assumption. Assumption. Assumption.
   Assumption. Assumption.
Qed.

Lemma until_mapmult_permmod:
   (p:nat)(a:Z)(Prime p)->~(Mod a `0` p)->
         (permmod p (until (pred p)) (mapmult a (until (pred p)))).
Proof.
   Intros.
   Apply nodoubles_allex_permmod.
   Assumption. Unfold mapmult. Apply map_length.
   Apply until_nodoubles. Assumption.
   Unfold allex. Intros.
   Apply (until_mapmult_allex p a H H0).
   Assumption.
Qed.

(* Fermat's Little Theorem. *)

Theorem flt:
   (a:Z)(p:nat)(Prime p)->~(Mod a `0` p)->(Mod (Exp a (pred p)) `1` p).
Proof.
   Intros. Apply mod_sym.
   Apply mod_mult_cancel_r with (zproduct (until (pred p))).
   Assumption. Apply until_prod_not_0mod. Assumption.
   Rewrite <- until_mapmult_exp. Rewrite Zmult_one.
   Apply permmod_product. Apply until_mapmult_permmod.
   Assumption. Assumption.
Qed.