Require Arith.
Require ZArith.
Require Wf_nat.

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

Transparent inject_nat.

(**
 * Some nice lemmas about div, mult, mod, prime, and gcd. 
 *)

Lemma prime_div_or_gcd1:
   (p:nat)(a:Z)(Prime p)->
      (ZDivides (inject_nat p) a)\/(gcd (inject_nat p) a (1)).
Proof.
   Intros. Elim (zdivdec a (inject_nat p)).
   Left. Assumption.
   Right. Unfold gcd. Unfold common_div.
   Split. Split.
   Split with p. Simpl. Rewrite <- plus_n_O. Apply abs_inj.
   Split with (absolu a). Simpl. Apply plus_n_O.
   Intros. Elim H1. Intros. Rewrite abs_inj in H2.
   Elim (primediv1p p e).
   Intro. Rewrite H4. Apply le_n.
   Intro. Rewrite H4 in H3. Elim H0. Apply divzdiv.
   Rewrite abs_inj. Assumption. Assumption. Assumption.
Qed.

Lemma divmultgcd:
   (a,b,c:Z)`a<>0`->(ZDivides a `b*c`)->(gcd a b (1))->(ZDivides a c).
Proof.
   Intros. Elim (gcd_lincomb a b (1)).
   Intro alpha. Intros. Elim H2. Intro beta. Intros.
   Elim H0. Intro y. Intros.
   Split with `c*alpha+y*beta`. Rewrite Zmult_plus_distr_r.
   Rewrite Zmult_assoc_l. Rewrite Zmult_assoc_l.
   Rewrite <- H4. Rewrite (Zmult_sym a c). Rewrite (Zmult_sym b c).
   Rewrite Zmult_assoc_r. Rewrite Zmult_assoc_r.
   Rewrite <- Zmult_plus_distr_r. Transitivity `c*1`.
   Rewrite Zmult_sym. Rewrite Zmult_one. Reflexivity.
   Apply (f_equal Z). Assumption. Assumption. Assumption.
Qed.

Lemma primedivmult:
   (p,n,m:nat)(Prime p)->
      (Divides p (mult n m))->(Divides p n)\/(Divides p m).
Proof.
   Intros. Elim (prime_div_or_gcd1 p (inject_nat n)).
   Left. Rewrite <- (abs_inj p). Rewrite <- (abs_inj n).
   Apply zdivdiv. Assumption.
   Right. Rewrite <- (abs_inj p). Rewrite <- (abs_inj m).
   Apply zdivdiv. Apply divmultgcd with (inject_nat n).
   Elim H. Intros. Apply Zgt_neq.
   Change `(inject_nat p) > (inject_nat O)`. Apply inj_gt.
   Apply gt_trans with (1). Assumption. Unfold gt. Unfold lt. Apply le_n.
   Rewrite <- inj_mult. Apply divzdiv. Rewrite abs_inj. Rewrite abs_inj.
   Assumption. Assumption. Assumption.
Qed.

Lemma mod_mult_inv_r:
   (a:Z)(p:nat)(Prime p)->~(Mod a `0` p)->(EX ra:Z | (Mod `a*ra` `1` p)).
Proof.
   Intros. Elim (prime_div_or_gcd1 p a).

   (* case p divides a *)
   Intro. Elim H0. Elim H1. Intros. Split with x. Simpl. Assumption.

   (* case gcd(p,a)=1 *)
   Intro. Elim (gcd_lincomb (inject_nat p) a (1)).
   Intro alpha. Intros. Elim H2. Intro beta. Intros.
   Unfold Mod. Split with beta. Split with `-alpha`.
   Simpl in H3. Rewrite H3.
   Rewrite (Zplus_sym `(inject_nat p)*alpha`). Rewrite Zplus_assoc_r.
   Rewrite <- Zmult_plus_distr_r. Rewrite Zplus_inverse_r.
   Rewrite <- Zmult_n_O. Rewrite <- Zplus_n_O. Reflexivity.
   Apply Zgt_neq. Change `(inject_nat p) > (inject_nat O)` .
   Apply inj_gt. Apply gt_trans with (1). Elim H. Intros. Assumption.
   Unfold gt. Unfold lt. Apply le_n.
   Assumption. Assumption.
Qed.

Lemma mod_mult_cancel_r:
   (a,b,c:Z; p:nat)(Prime p)->~(Mod c `0` p)->
      (Mod `a*c` `b*c` p)->(Mod a b p).
Proof.
   Intros. Elim (mod_mult_inv_r c p). Intro rc. Intros.
   Apply mod_trans with `a*c*rc`. Rewrite Zmult_assoc_r.
   Pattern 1 a. Replace a with `a*1`. Apply mod_mult_compat. Apply mod_refl.
   Apply mod_sym. Assumption.
   Rewrite Zmult_sym. Apply Zmult_one.
   Apply mod_trans with `b*c*rc`.
   Apply mod_mult_compat. Assumption. Apply mod_refl. Rewrite Zmult_assoc_r.
   Pattern 2 b. Replace b with `b*1`. Apply mod_mult_compat. Apply mod_refl.
   Assumption.
   Rewrite Zmult_sym. Apply Zmult_one.
   Assumption. Assumption.
Qed.

Lemma mod_mult_0:
   (p:nat)(a,b:Z)(Prime p)->
      (Mod `a*b` `0` p)->(Mod a `0` p)\/(Mod b `0` p).
Proof.
   Intros. Elim (moddivmin `a*b` `0` p). Rewrite <- Zminus_n_O.
   Rewrite abs_mult. Intros.
   Elim (primedivmult p (absolu a) (absolu b)).

   Left. Elim H3. Intros.
   Elim (Zle_or_lt `0` a).

   (* case 0 <= a *)
   Intro. Split with (inject_nat x).
   Simpl. Rewrite <- inj_mult. Rewrite <- H4.
   Rewrite inj_abs_pos. Reflexivity. Apply Zle_ge. Assumption.

   (* case a < 0 *)
   Intro. Split with `-(inject_nat x)`.
   Simpl. Rewrite <- Zmult_Zopp_left. Rewrite Zopp_Zmult.
   Rewrite <- inj_mult. Rewrite <- H4.
   Rewrite inj_abs_neg. Rewrite Zopp_Zopp. Reflexivity. Assumption.

   Right. Elim H3. Intros.
   Elim (Zle_or_lt `0` b).

   (* case 0 <= b *)
   Intro. Split with (inject_nat x).
   Simpl. Rewrite <- inj_mult. Rewrite <- H4.
   Rewrite inj_abs_pos. Reflexivity. Apply Zle_ge. Assumption.

   (* case a < 0 *)
   Intro. Split with `-(inject_nat x)`.
   Simpl. Rewrite <- Zmult_Zopp_left. Rewrite Zopp_Zmult.
   Rewrite <- inj_mult. Rewrite <- H4.
   Rewrite inj_abs_neg. Rewrite Zopp_Zopp. Reflexivity. Assumption.

   Assumption.
   Apply H1. Assumption.
Qed.


(**
 * Fermat's little theorem.
 *)

Axiom fermats_little2:
   (a:Z)(p:nat)(Prime p)->~(Mod a `0` p)->(Mod (Exp a (pred p)) `1` p).

(* (permMod p l1 l2) means l2 is a permutation of l1 modulo p *)

Fixpoint permMod [p:nat; l1:Zlist]: Zlist->Prop :=
   [l2:Zlist]
   Cases l1 of
      Nil         => Cases l2 of
                        Nil        => True
                      | (Cons _ _) => False
                     end      
    | (Cons x xs) => (EX x':Z | (inlist Z x' l2) /\
                                (Mod x x' p) /\
                                (permMod p xs (zdrop x' l2)))
   end.

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. Simpl.
   Split with x2.
   Split. Unfold inlist. Simpl. Left. Reflexivity.
   Split. Assumption.
   Elim (zeq_bool_eq x2 x2). Intros.
   Rewrite H1.
   Assumption.
   Reflexivity.
Qed.

Lemma permmod_same_length:
   (p:nat; l1,l2:Zlist)(permMod p l1 l2)->(length Z l1)=(length Z l2).
Proof.
   Induction l1.
   Induction l2. Simpl. Reflexivity.
   Intros y ys IH2. Simpl. Intros. Elim H.
   Intros x xs IH1. Intros.
   Elim H. Intros. Elim H0. Intros. Elim H2. Intros.
   Simpl. Rewrite (IH1 (zdrop x0 l2)). Apply length_zdrop.
   Assumption. Assumption.
Qed.

Lemma permmod_not_nil_cons:
   (p:nat; h:Z; t:Zlist)~(permMod p (Nil Z) (Cons Z h t)).
Proof.
   Unfold permMod. Intros. Intro. Assumption.
Qed.

(*

Lemma permmod_cons_zdrop:
   (p:nat; x:Z; l:Zlist)
      (inlist Z x l)->(permMod p l (Cons Z x (zdrop x l))).
Proof.
   Induction l. Unfold inlist. Simpl. Intro. Assumption.
   Intros h t IH. Elim (zeqdec x h).
   Intro. Rewrite (zdrop_head_eq x h).
   Intros. Rewrite H. Apply permmod_refl. Assumption.
   Intro. Rewrite (zdrop_head_neq x h).
   Intros.


*)

(*

Lemma permmod_zdrop_simpl:
   (p:nat; x1,x2:Z; l1,l2:Zlist)
      (permMod p l1 l2) -> (Mod x1 x2 p) ->
         (permMod p (zdrop x1 l1) (zdrop x2 l2)).
Proof.
   Induction l1.

   (* case l1=Nil *)
   Induction l2.
   Simpl. Intros. Trivial.
   Intros. Cut (length Z (Nil Z))=(length Z (Cons Z y l)).
   Simpl. Intro. Discriminate H2.
   Apply permmod_same_length with p. Assumption.

   (* case l1=(Cons h1 t1) *)
   Intros h1 t1 IH1.
   Induction l2.
   Intros. Cut (length Z (Cons Z h1 t1))=(length Z (Nil Z)).
   Simpl. Intro. Discriminate H1.
   Apply permmod_same_length with p. Assumption.
   Intros h2 t2 IH2. Intros. Elim H. Intro h1'. Intros.
   Elim H1. Intros. Elim H3. Intros.

   Elim (zeqdec x1 h1).

      (* case x1=h1 *)
      Intro. Rewrite H6. Rewrite zdrop_head_eq.
      Elim (zeqdec x2 h1').

         (* case x2=h1' *)
         Intro. Rewrite H7. Assumption.

         (* case x2<>h1' *)
         Intro. Rewrite zdrop_head_neq. Rewrite <- (zdrop_head_eq x1 h1 t1).
         
*)
   
(*

Lemma permmod_ok:
   (p:nat; l1,l2:Zlist)
      (length Z l1)=(length Z l2) /\
      ((x:Z)(inlist Z x l1)->
         (EX x':Z | (inlist Z x' l2) /\
                    (Mod x x' p) /\
                    (permMod p (zdrop x l1) (zdrop x' l2))))<->
      (permMod p l1 l2).
Proof.
   Induction l1.

   (* case l1=Nil *)
   Induction l2.
   Simpl. Split.
   Intros. Trivial.
   Intros. Split. Reflexivity.
   Intros. Unfold inlist in H0. Simpl in H0. Elim H0.
   Intros h2 t2 IH2. Elim IH2.  Intros. Split.
   Intros.Elim H1. Intros. Simpl in H2. Discriminate H2.
   Intros. Cut (length Z (Nil Z))=(length Z (Cons Z h2 t2)).
   Intros. Discriminate H2. Apply permmod_same_length with p.
   Assumption.

   (* case l1=(Cons h1 t1) *)
   Intros h1 t1 IH1.
   Induction l2.
   Simpl. Split.

   (* -> *)
   Intros. Elim H. Intros. Discriminate H0.
   Intros. Elim H. Intros. Elim H0. Intros.
   Unfold inlist in H1. Simpl in H1. Elim H1.
   Intros h2 t2 IH2. Split.
   Intros. Elim H. Intros. Elim (H1 h1).
   Intro h1'. Intros.
   Elim H2.  Intros. Elim H4. Intros.
   Elim (zeqdec h1' h2).

      (* case h1'=h2 *)
      Intro. Split with h1'.
      Split. Unfold inlist. Rewrite H7.
      Simpl. Left. Reflexivity.
      Split. Assumption.
      Rewrite H7. Rewrite zdrop_head_eq.
      Rewrite zdrop_head_eq in H6. Rewrite zdrop_head_eq in H6.
      Assumption. Assumption. Reflexivity. Reflexivity.

      (* case h1'<>h2 *)
      Intro. Split with h1'.
      Split. Assumption.
      Split. Assumption.
      Rewrite <- (zdrop_head_eq h1 h1 t1).
      Assumption.
      Reflexivity.
      Apply inlist_head_eq. Reflexivity.

   (* <- *)
   Intros. Split.
   Apply permmod_same_length with p. Assumption.
   Intros. Elim H. Intro h1'. Intros.
   Elim H1. Intros. Elim H3. Intros.
   Elim (zeqdec x h1).

      (* case x=h1 *)
      Intro. Split with h1'.
      Split. Assumption.
      Split. Rewrite H6. Assumption.
      Rewrite H6. Rewrite zdrop_head_eq.
      Assumption. Reflexivity.

      (* case x<>h1 *)
      Intro. Elim (IH1 (zdrop h1' (Cons Z h2 t2))).
      Intros. Elim H8. Intros. Elim (H10 x).
      Intro x'. Intros. Elim H11. Intros. Elim H13. Intros.
      Split with x'.
      Split. Apply zdrop_inlist_preserve with h1'.
      Assumption.
      Split. Assumption.

      Elim (zeqdec x' h2).
      Intro. Rewrite (zdrop_head_eq x'). Rewrite (zdrop_head_neq x).

Lemma permmod_ok:
   (p:nat; l1,l2:Zlist)
      (length Z l1)=(length Z l2)->
         ((x:Z)(inlist Z x l1)->
            (EX x':Z | (inlist Z x' l2) /\
                       (Mod x x' p) /\
                       (permMod p (zdrop x l1) (zdrop x' l2))))->
            (permMod p l1 l2).
Proof.
   Induction l1.

   (* case l1=Nil *)
   Induction l2.
   Simpl. Intros. Trivial.
   Simpl. Intros. Discriminate H0.

   (* case l1=(Cons h1 t1) *)
   Intros h1 t1 IH1.
   Induction l2.
   Simpl. Intros. Discriminate H.
   Intros h2 t2 IH2.
   Intros.
   Elim (H0 h1). Intro h1'. Intros. Elim H1.
   Intros. Elim H3. Intros.
   Elim (zeqdec h1' h2).

      (* case h1'=h2 *)
      Intro. Split with h2.
      Split. Unfold inlist. Simpl. Left. Reflexivity.
      Split. Apply mod_trans with h1'. Assumption.
      Rewrite H6. Apply mod_refl.
      Rewrite zdrop_head_eq.
      Rewrite zdrop_head_eq in H5. Rewrite zdrop_head_eq in H5.
      Assumption. Assumption. Reflexivity. Reflexivity.
   
      (* case h1'<>h2 *)
      Intro. Split with h1'.
      Split. Assumption.
      Split. Assumption.
      Rewrite <- (zdrop_head_eq h1 h1 t1).
      Assumption.
      Reflexivity.
      Apply inlist_head_eq. Reflexivity.
Qed.

*)

Lemma permmod_refl:
   (l:Zlist; p:nat)(permMod p l l).
Proof.
   Induction l.
   Simpl. Intro. Trivial.
   Intros h t IH. Simpl. Intros.
   Unfold inlist. Simpl. Split with h.
   Split. Left. Reflexivity.
   Split. Apply mod_refl.
   Elim (zeq_bool_eq h h). Intros. Rewrite H.
   Apply IH. Reflexivity.
Qed.

Lemma permmod_cons_cons:
   (p:nat; x,y:Z; l:Zlist)
     (permMod p (Cons Z x (Cons Z y l)) (Cons Z y (Cons Z x l))).
Proof.
   Intros. Elim (zeqdec x y).
   Intro. Rewrite H. Apply permmod_refl.
   Intro.
   Split with x.
   Split. Apply inlist_tail. Apply inlist_head_eq. Reflexivity.
   Split. Apply mod_refl.
   Split with y.
   Split. Rewrite zdrop_head_neq.
   Apply inlist_head_eq. Reflexivity.
   Assumption.
   Split. Apply mod_refl.
   Rewrite zdrop_head_neq. Rewrite zdrop_head_eq.
   Rewrite zdrop_head_eq. Apply permmod_refl.
   Reflexivity. Reflexivity. Assumption.
Qed.

(*

Lemma permmod_trans:
   (l1,l2,l3:Zlist; p:nat)
      (permMod p l1 l2)->
         (permMod p l2 l3)->
            (permMod p l1 l3).
Proof.
   Intros.
   Apply permmod_ok. Transitivity (length Z l2).
   Apply permmod_same_length with p. Assumption.
   Apply permmod_same_length with p. Assumption.
   Intros.

   Induction l1.
   (* base l1 *)
      Induction l2.
      (* base l2 *)
         Intros. Assumption.
      (* step l2 *)
         Intros h2 t2 IH2.
         Induction l3.
         (* base l3 *)
            Intros. Simpl. Trivial.
         (* step l3 *)
            Intros h3 t3 IH3. Simpl. Intros. Elim H.
   (* step l1 *)
      Intros h1 t1 IH1.
      Induction l2.
      (* base l2 *)
         Induction l3.
         (* base l3 *)
            Simpl. Intros. Assumption.
         (* step l3 *)
            Simpl. Intros. Elim H1.
       (* step l2 *)
         Intros h2 t2 IH2.
         Induction l3.
         (* base l3 *)
            Simpl. Unfold inlist. Simpl. Intros. 
            Elim H0. Intros. Elim H1. Intros.
            Elim H3. Intros. Elim H4.
         (* step l3 *)
            Intros h3 t3 IH3. Simpl. Intros.
            Elim H. Intros. Elim H0. Intros.
            Elim H1. Intros. Elim H3. Intros.
            Elim H5. Intros. Elim H6. Intros.
            Split.
*)


(*

Lemma permmod_sym:
   (l1,l2:Zlist; p:nat)(permMod p l1 l2)->(permMod p l2 l1).
Proof.
   Induction l1.

   (* l1=Nil *)
   Induction l2.
   Simpl. Intros. Assumption.
   Intros h2 t2 IH2. Simpl. Intros. Elim H.

   (* l1=(Cons h1 t1) *)
   Intros h1 t1 IH1.
   Induction l2.
   Simpl. Unfold inlist. Simpl. Intros.
   Elim H. Intros. Elim H0. Intro. Elim H1.
   Intros h2 t2 IH2. Intros.
   Elim H. Intro h1'. Intros.
   Elim H0. Intros. Elim H2. Intros.
   Elim (zeqdec h1' h2).

      (* case h1'=h2 *)
      Intro. Apply permmod_cons_extend.
      Apply (IH1 t2). Rewrite zdrop_head_eq in H4.
      Assumption. Assumption.
      Rewrite <- H5. Apply mod_sym. Assumption.

      (* case h1'<>h2 *)
      Intro. Rewrite (zdrop_head_neq h1' h2) in H4.
      Elim (IH1 (Cons Z h2 (zdrop h1' t2)) p H4).
      Intro h2'. Intros.
      Elim H6. Intros. Elim H8. Intros.
      Split with h2'.
      Split. Apply inlist_tail. Assumption.
      Split. Assumption.
      Elim (zeqdec h2' h1).

         (* case h2'=h1 *)
         Intro. Rewrite (zdrop_head_eq h2').
         Apply (IH1 t2).


*)


(*

Lemma permmod_hddrop:
   (x:Z; l:Zlist; p:nat)
      (inlist Z x l) -> (permMod p l (Cons Z x (zdrop x l))).

Lemma permmod_cons_simpl:
   (x,x':Z; t,r:Zlist; p:nat)
      (Mod x x' p)->
         (permMod p (Cons Z x t) (Cons Z x' r))->
            (permMod p t r).

Lemma permmod_cons_drop_simpl:
   (x:Z; l1,l2:Zlist; p:nat)
      (permMod p (Cons Z x l1) l2)->
         (EX x':Z | (Mod x x' p) /\ (permMod p l1 (zdrop x' l2))).
*)



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

(* (until (pred p)) represents all non-zero integers modulo p *)

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.

(* There is no 0 in (until (pred p)) *)

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.


(**
 * The order of elements in the multgroup modulo p.
 * (Order b q p) means the order of b is q in multgroup(Z_p).
 *)

Definition Order :=
   [b:Z][q,p:nat](lt O q) /\
      (Mod (Exp b q) `1` p) /\
         ((d:nat)(lt O d)->(Mod (Exp b d) `1` p)->(le q d)).

Lemma orderdec: (b:Z; q,p:nat)(Order b q p)\/~(Order b q p).
Proof.
   Intros. Unfold Order.
   Apply anddec.
   Apply ltdec.
   Apply anddec.
   Apply moddec.
   Elim (exdec [d:nat](lt O d)/\(Mod (Exp b d) `1` p) q).
   Right. Intros.
   Elim H.
   Intro d.
   Intros.
   Elim H0. Intros.
   Elim H2. Intros.
   Intro.
   Elim (le_not_lt q d).
   Apply H5.
   Assumption.
   Assumption.
   Assumption.
   Left. Intros.
   Elim (le_or_lt q d).
   Intro. Assumption.
   Intro.
   Elim H.
   Split with d.
   Split.
   Assumption.
   Split.
   Assumption.
   Assumption.
   Intro.
   Apply anddec.
   Apply ltdec.
   Apply moddec.
Qed.

Lemma order_ex1: (b:Z)(p:nat)(Prime p)->
                    (EX d:nat | (lt O d)/\(Mod (Exp b d) `1` p))->
                       (EX x:nat | (Order b x p)).
Proof.
   Intros. Elim H0.
   Intro. Apply (lt_wf_ind x).
   Intros X IH.
   Intros.
   Elim (exdec [m:nat](lt O m)/\(Mod (Exp b m) `1` p) X).
   Intro.
   Elim H2. 
   Intros.
   Elim H3. Intros.
   Elim H5. Intros.
   Elim (IH x0). Intros.
   Split with x1.
   Assumption.
   Assumption.
   Split. Assumption. Assumption.
   Intros. Split with X.
   Elim H1. Intros.
   Split.
   Assumption.
   Split.
   Assumption.
   Intros.
   Elim (le_or_lt X d).
   Intro. Assumption.
   Intros.
   Elim H2.
   Split with d.
   Split.
   Assumption.
   Split.
   Assumption.
   Assumption.
   Intro. Apply anddec. Apply ltdec. Apply moddec.
Qed.

Lemma order_ex: (b:Z)(p:nat)(Prime p)->~(Mod b `0` p)->
                   (EX x:nat | (lt x p) /\ (Order b x p)).
Proof.
   Intros.
   Elim H.
   Intros.
   Elim (order_ex1 b p H).
   Intros.
   Split with x.
   Split.
   Apply le_lt_trans with (pred p).
   Elim H3.
   Intros.
   Elim H5.
   Intros.
   Apply (H7 (pred p)).
   Apply lt_pred.
   Assumption.
   Apply fermats_little2. Assumption. Assumption.
   Apply lt_pred_n_n.
   Apply lt_trans with (1). Apply lt_O_Sn. Assumption.
   Assumption.
   Split with (pred p).
   Split.
   Apply lt_pred.
   Assumption.
   Apply fermats_little2. Assumption. Assumption.
Qed.

Lemma order_div:
   (b:Z)(x,p:nat)(Order b x p) ->
      (y:nat)(lt O y)->(Mod (Exp b y) `1` p)->(Divides x y).
Proof.
   Intros.
   Elim H. Intros.
   Elim H3. Intros.
   Elim (divdec y x). Intro. Assumption. Intro.
   Elim (notdiv_rem x y H2 H6).
   Intro q. Intros. Elim H7. Intro r. Intros.
   Elim H8. Intros. Elim H10. Intros.
   Rewrite H12 in H1.
   Elim (lt_not_le r x).
   Assumption.
   Apply H5.
   Assumption.
   Apply mod_trans with `(Exp b (mult q x))*(Exp b r)`.
   Apply mod_trans with `(Exp (Exp b x) q)*(Exp b r)`.
   Pattern 1 (Exp b r).
   Replace (Exp b r) with `1*(Exp b r)`.
   Apply mod_mult_compat.
   Apply mod_sym.
   Apply mod_exp1.
   Assumption.
   Apply mod_refl.
   Apply Zmult_one.
   Rewrite mult_sym.
   Rewrite exp_mult.
   Apply mod_refl.
   Rewrite <- exp_plus.
   Assumption.
Qed.

Lemma order_le_predp:
   (b:Z)(q,p:nat)(Prime p)->(Order b q p)->(le q (pred p)).
Proof.
   Intros.
   Elim H. Intros.
   Elim H0. Intros.
   Elim H4. Intros.
   Apply H6.
   Apply lt_pred. Assumption.
   Apply fermats_little2.
   Assumption.
   Intro.
   Elim (mod_0not1 p).
   Assumption.
   Apply mod_trans with (Exp b q).
   Apply mod_sym.
   Apply moda0_exp_compat.
   Unfold gt.
   Unfold gt in H1.
   Unfold lt.
   Apply lt_le_weak.
   Assumption.
   Assumption.
   Assumption.
   Assumption.
Qed.

Lemma mod_ab0a0b0:
   (p:nat)(Prime p)->(a,b:Z)(Mod `a*b` `0` p)->(Mod a `0` p)\/(Mod b `0` p).
Proof.
   Intros.
   Elim (moddivmin `a*b` `0` p).
   Intros.
   Rewrite <- Zminus_n_O in H1.
   Rewrite abs_mult in H1.
   Elim (primedivmult p (absolu a) (absolu b)).
   Left. Elim (moddivmin a `0` p). Intros.
   Apply H5. Rewrite <- Zminus_n_O. Assumption.
   Right. Elim (moddivmin b `0` p). Intros.
   Apply H5. Rewrite <- Zminus_n_O. Assumption.
   Assumption.
   Apply H1.
   Assumption.
Qed.

Lemma mod_not_exp_0:
   (p:nat)(Prime p)->
      (a:Z)~(Mod a `0` p) -> (m:nat)~(Mod (Exp a m) `0` p).
Proof.
   Intros p Hp a Ha. Induction m.
   Simpl. Intro. Elim (mod_0not1 p).
   Elim Hp. Intros. Assumption.
   Apply mod_sym. Assumption.
   Simpl. Intros. Intro.
   Elim (mod_ab0a0b0 p Hp a (Exp a n)).
   Assumption. Assumption. Assumption.
Qed.