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


(**
   order.
   The order of elements in the multgroup modulo p.
 
   @author Olga Caprotti and Martijn Oostdijk
   @version $Revision$
*)

Require Import Arith.
Require Import ZArith.
Require Import Wf_nat.

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.
Require Import fermat.

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

Definition Order (b : Z) (q p : nat) :=
  0 < q /\
  Mod (Exp b q) 1 p /\ (forall d : nat, 0 < d -> Mod (Exp b d) 1 p -> q <= d).

Lemma orderdec : forall (b : Z) (q p : nat), Order b q p \/ ~ Order b q p.
Proof.
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   intros. unfold Order in |- *.
(* Goal: or (and (lt O n) (Mod (Exp b n) (Zpos xH) p)) (not (and (lt O n) (Mod (Exp b n) (Zpos xH) p))) *)
   apply anddec.
(* Goal: or (lt O n) (not (lt O n)) *)
(* Goal: or (Mod (Exp b n) (Zpos xH) p) (not (Mod (Exp b n) (Zpos xH) p)) *)
   apply ltdec.
(* Goal: or (and (lt O n) (Mod (Exp b n) (Zpos xH) p)) (not (and (lt O n) (Mod (Exp b n) (Zpos xH) p))) *)
   apply anddec.
(* Goal: or (Mod (Exp b n) (Zpos xH) p) (not (Mod (Exp b n) (Zpos xH) p)) *)
   apply moddec.
(* Goal: or (forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d) (not (forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d)) *)
   elim (exdec (fun d : nat => 0 < d /\ Mod (Exp b d) 1 p) q).
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   right. intros.
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   elim H. intro d. intros.
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   elim H0. intros.
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   elim H2. intros.
(* Goal: not (Mod b Z0 p) *)
   intro. elim (le_not_lt q d).
(* Goal: le x r *)
   apply H5.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   assumption.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   assumption.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   assumption.
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   left. intros.
(* Goal: le q d *)
(* Goal: forall n : nat, or (and (lt O n) (Mod (Exp b n) (Zpos xH) p)) (not (and (lt O n) (Mod (Exp b n) (Zpos xH) p))) *)
   elim (le_or_lt q d).
(* Goal: not (Mod b Z0 p) *)
   intro. assumption.
(* Goal: not (Mod b Z0 p) *)
   intro.
(* Goal: le q (Init.Nat.pred p) *)
   elim H.
(* Goal: @ex nat (fun x : nat => and (lt x X) (and (lt O x) (Mod (Exp b x) (Zpos xH) p))) *)
(* Goal: forall n : nat, or (and (lt O n) (Mod (Exp b n) (Zpos xH) p)) (not (and (lt O n) (Mod (Exp b n) (Zpos xH) p))) *)
   split with d.
(* Goal: and (lt O (Init.Nat.pred p)) (Mod (Exp b (Init.Nat.pred p)) (Zpos xH) p) *)
   split.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   assumption.
(* Goal: and (lt O (Init.Nat.pred p)) (Mod (Exp b (Init.Nat.pred p)) (Zpos xH) p) *)
   split.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   assumption.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   assumption.
(* Goal: not (Mod b Z0 p) *)
   intro.
(* Goal: or (and (lt O n) (Mod (Exp b n) (Zpos xH) p)) (not (and (lt O n) (Mod (Exp b n) (Zpos xH) p))) *)
   apply anddec.
(* Goal: or (lt O n) (not (lt O n)) *)
(* Goal: or (Mod (Exp b n) (Zpos xH) p) (not (Mod (Exp b n) (Zpos xH) p)) *)
   apply ltdec.
(* Goal: or (Mod (Exp b n) (Zpos xH) p) (not (Mod (Exp b n) (Zpos xH) p)) *)
   apply moddec.
Qed.

Lemma order_ex1 :
 forall (b : Z) (p : nat),
 Prime p ->
 (exists d : nat, 0 < d /\ Mod (Exp b d) 1 p) -> exists x : nat, Order b x p.
Proof.
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   intros. elim H0.
(* Goal: not (Mod b Z0 p) *)
   intro. apply (lt_wf_ind x).
(* Goal: forall (n : nat) (_ : forall (m : nat) (_ : lt m n) (_ : and (lt O m) (Mod (Exp b m) (Zpos xH) p)), @ex nat (fun x : nat => Order b x p)) (_ : and (lt O n) (Mod (Exp b n) (Zpos xH) p)), @ex nat (fun x : nat => Order b x p) *)
   intros X IH.
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   intros.
(* Goal: @ex nat (fun x : nat => Order b x p) *)
   elim (exdec (fun m : nat => 0 < m /\ Mod (Exp b m) 1 p) X).
(* Goal: not (Mod b Z0 p) *)
   intro.
(* Goal: le X d *)
(* Goal: forall n : nat, or (and (lt O n) (Mod (Exp b n) (Zpos xH) p)) (not (and (lt O n) (Mod (Exp b n) (Zpos xH) p))) *)
   elim H2. 
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   intros.
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   elim H3. intros.
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   elim H5. intros.
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   elim (IH x0). intros.
(* Goal: @ex nat (fun x : nat => Order b x p) *)
(* Goal: lt x0 X *)
(* Goal: and (lt O x0) (Mod (Exp b x0) (Zpos xH) p) *)
(* Goal: forall _ : not (@ex nat (fun x : nat => and (lt x X) (and (lt O x) (Mod (Exp b x) (Zpos xH) p)))), @ex nat (fun x : nat => Order b x p) *)
(* Goal: forall n : nat, or (and (lt O n) (Mod (Exp b n) (Zpos xH) p)) (not (and (lt O n) (Mod (Exp b n) (Zpos xH) p))) *)
   split with x1.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   assumption.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   assumption.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   split. assumption. assumption.
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   intros. split with X.
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   elim H1. intros.
(* Goal: and (lt O (Init.Nat.pred p)) (Mod (Exp b (Init.Nat.pred p)) (Zpos xH) p) *)
   split.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   assumption.
(* Goal: and (lt O (Init.Nat.pred p)) (Mod (Exp b (Init.Nat.pred p)) (Zpos xH) p) *)
   split.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   assumption.
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   intros.
(* Goal: le X d *)
(* Goal: forall n : nat, or (and (lt O n) (Mod (Exp b n) (Zpos xH) p)) (not (and (lt O n) (Mod (Exp b n) (Zpos xH) p))) *)
   elim (le_or_lt X d).
(* Goal: not (Mod b Z0 p) *)
   intro. assumption.
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   intros.
(* Goal: le X d *)
(* Goal: forall n : nat, or (and (lt O n) (Mod (Exp b n) (Zpos xH) p)) (not (and (lt O n) (Mod (Exp b n) (Zpos xH) p))) *)
   elim H2.
(* Goal: @ex nat (fun x : nat => and (lt x X) (and (lt O x) (Mod (Exp b x) (Zpos xH) p))) *)
(* Goal: forall n : nat, or (and (lt O n) (Mod (Exp b n) (Zpos xH) p)) (not (and (lt O n) (Mod (Exp b n) (Zpos xH) p))) *)
   split with d.
(* Goal: and (lt O (Init.Nat.pred p)) (Mod (Exp b (Init.Nat.pred p)) (Zpos xH) p) *)
   split.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   assumption.
(* Goal: and (lt O (Init.Nat.pred p)) (Mod (Exp b (Init.Nat.pred p)) (Zpos xH) p) *)
   split.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   assumption.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   assumption.
(* Goal: or (and (lt O n) (Mod (Exp b n) (Zpos xH) p)) (not (and (lt O n) (Mod (Exp b n) (Zpos xH) p))) *)
   intro. apply anddec. apply ltdec. apply moddec.
Qed.

Lemma order_ex :
 forall (b : Z) (p : nat),
 Prime p -> ~ Mod b 0 p -> exists x : nat, x < p /\ Order b x p.
Proof.
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   intros.
(* Goal: le q (Init.Nat.pred p) *)
   elim H.
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   intros.
(* Goal: @ex nat (fun x : nat => and (lt x p) (Order b x p)) *)
   elim (order_ex1 b p H).
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   intros.
(* Goal: @ex nat (fun x : nat => and (lt x p) (Order b x p)) *)
(* Goal: @ex nat (fun d : nat => and (lt O d) (Mod (Exp b d) (Zpos xH) p)) *)
   split with x.
(* Goal: and (lt O (Init.Nat.pred p)) (Mod (Exp b (Init.Nat.pred p)) (Zpos xH) p) *)
   split.
(* Goal: lt x p *)
(* Goal: Order b x p *)
(* Goal: @ex nat (fun d : nat => and (lt O d) (Mod (Exp b d) (Zpos xH) p)) *)
   apply le_lt_trans with (pred p).
(* Goal: Divides x y *)
   elim H3.
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   intros.
(* Goal: le x (Init.Nat.pred p) *)
(* Goal: lt (Init.Nat.pred p) p *)
(* Goal: Order b x p *)
(* Goal: @ex nat (fun d : nat => and (lt O d) (Mod (Exp b d) (Zpos xH) p)) *)
   elim H5.
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   intros.
(* Goal: le x (Init.Nat.pred p) *)
(* Goal: lt (Init.Nat.pred p) p *)
(* Goal: Order b x p *)
(* Goal: @ex nat (fun d : nat => and (lt O d) (Mod (Exp b d) (Zpos xH) p)) *)
   apply (H7 (pred p)).
(* Goal: lt O (Init.Nat.pred p) *)
(* Goal: Mod (Exp b (Init.Nat.pred p)) (Zpos xH) p *)
   apply lt_pred.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   assumption.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   apply flt. assumption. assumption.
(* Goal: lt (Init.Nat.pred p) p *)
(* Goal: Order b x p *)
(* Goal: @ex nat (fun d : nat => and (lt O d) (Mod (Exp b d) (Zpos xH) p)) *)
   apply lt_pred_n_n.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   apply lt_trans with 1. apply lt_O_Sn. assumption.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   assumption.
(* Goal: @ex nat (fun d : nat => and (lt O d) (Mod (Exp b d) (Zpos xH) p)) *)
   split with (pred p).
(* Goal: and (lt O (Init.Nat.pred p)) (Mod (Exp b (Init.Nat.pred p)) (Zpos xH) p) *)
   split.
(* Goal: lt O (Init.Nat.pred p) *)
(* Goal: Mod (Exp b (Init.Nat.pred p)) (Zpos xH) p *)
   apply lt_pred.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   assumption.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   apply flt. assumption. assumption.
Qed.

Lemma order_div :
 forall (b : Z) (x p : nat),
 Order b x p -> forall y : nat, 0 < y -> Mod (Exp b y) 1 p -> Divides x y.
Proof.
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   intros.
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   elim H. intros.
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   elim H3. intros.
(* Goal: not (Mod b Z0 p) *)
   elim (divdec y x). intro. assumption. intro.
(* Goal: Divides x y *)
   elim (notdiv_rem x y H2 H6).
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   intro q. intros. elim H7. intro r. intros.
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   elim H8. intros. elim H10. intros.
(* Goal: Divides x y *)
   rewrite H12 in H1.
(* Goal: Divides x y *)
   elim (lt_not_le r x).
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   assumption.
(* Goal: le x r *)
   apply H5.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   assumption.
(* Goal: Mod (Exp b r) (Zpos xH) p *)
   apply mod_trans with (Exp b (q * x) * Exp b r)%Z.
(* Goal: Mod (Exp b r) (Z.mul (Exp b (Init.Nat.mul q x)) (Exp b r)) p *)
(* Goal: Mod (Z.mul (Exp b (Init.Nat.mul q x)) (Exp b r)) (Zpos xH) p *)
   apply mod_trans with (Exp (Exp b x) q * Exp b r)%Z.
(* Goal: Mod (Exp b r) (Z.mul (Exp (Exp b x) q) (Exp b r)) p *)
(* Goal: Mod (Z.mul (Exp (Exp b x) q) (Exp b r)) (Z.mul (Exp b (Init.Nat.mul q x)) (Exp b r)) p *)
(* Goal: Mod (Z.mul (Exp b (Init.Nat.mul q x)) (Exp b r)) (Zpos xH) p *)
   pattern (Exp b r) at 1 in |- *.
(* Goal: (fun z : Z => Mod z (Z.mul (Exp (Exp b x) q) (Exp b r)) p) (Exp b r) *)
(* Goal: Mod (Z.mul (Exp (Exp b x) q) (Exp b r)) (Z.mul (Exp b (Init.Nat.mul q x)) (Exp b r)) p *)
(* Goal: Mod (Z.mul (Exp b (Init.Nat.mul q x)) (Exp b r)) (Zpos xH) p *)
   replace (Exp b r) with (1 * Exp b r)%Z.
(* Goal: Mod (Z.mul (Zpos xH) (Exp b r)) (Z.mul (Exp (Exp b x) q) (Exp b r)) p *)
(* Goal: @eq Z (Z.mul (Zpos xH) (Exp b r)) (Exp b r) *)
(* Goal: Mod (Z.mul (Exp (Exp b x) q) (Exp b r)) (Z.mul (Exp b (Init.Nat.mul q x)) (Exp b r)) p *)
(* Goal: Mod (Z.mul (Exp b (Init.Nat.mul q x)) (Exp b r)) (Zpos xH) p *)
   apply mod_mult_compat.
(* Goal: Mod Z0 (Exp b q) p *)
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   apply mod_sym.
(* Goal: Mod (Exp (Exp b x) q) (Zpos xH) p *)
(* Goal: Mod (Exp b r) (Exp b r) p *)
(* Goal: @eq Z (Z.mul (Zpos xH) (Exp b r)) (Exp b r) *)
(* Goal: Mod (Z.mul (Exp (Exp b x) q) (Exp b r)) (Z.mul (Exp b (Init.Nat.mul q x)) (Exp b r)) p *)
(* Goal: Mod (Z.mul (Exp b (Init.Nat.mul q x)) (Exp b r)) (Zpos xH) p *)
   apply mod_exp1.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   assumption.
(* Goal: Mod (Z.mul (Exp (Exp b x) q) (Exp b r)) (Z.mul (Exp (Exp b x) q) (Exp b r)) p *)
(* Goal: Mod (Z.mul (Exp b (Init.Nat.mul q x)) (Exp b r)) (Zpos xH) p *)
   apply mod_refl.
(* Goal: @eq Z (Z.mul (Zpos xH) (Exp b r)) (Exp b r) *)
(* Goal: Mod (Z.mul (Exp (Exp b x) q) (Exp b r)) (Z.mul (Exp b (Init.Nat.mul q x)) (Exp b r)) p *)
(* Goal: Mod (Z.mul (Exp b (Init.Nat.mul q x)) (Exp b r)) (Zpos xH) p *)
   apply Zmult_1_l.
(* Goal: Mod (Z.mul (Exp (Exp b x) q) (Exp b r)) (Z.mul (Exp b (Init.Nat.mul q x)) (Exp b r)) p *)
(* Goal: Mod (Z.mul (Exp b (Init.Nat.mul q x)) (Exp b r)) (Zpos xH) p *)
   rewrite mult_comm.
(* Goal: Mod (Z.mul (Exp (Exp b x) q) (Exp b r)) (Z.mul (Exp b (Nat.mul x q)) (Exp b r)) p *)
(* Goal: Mod (Z.mul (Exp b (Init.Nat.mul q x)) (Exp b r)) (Zpos xH) p *)
   rewrite exp_mult.
(* Goal: Mod (Z.mul (Exp (Exp b x) q) (Exp b r)) (Z.mul (Exp (Exp b x) q) (Exp b r)) p *)
(* Goal: Mod (Z.mul (Exp b (Init.Nat.mul q x)) (Exp b r)) (Zpos xH) p *)
   apply mod_refl.
(* Goal: Mod (Z.mul (Exp b (Init.Nat.mul q x)) (Exp b r)) (Zpos xH) p *)
   rewrite <- exp_plus.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   assumption.
Qed.

Lemma order_le_predp :
 forall (b : Z) (q p : nat), Prime p -> Order b q p -> q <= pred p.
Proof.
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   intros.
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   elim H. intros.
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   elim H0. intros.
(* Goal: forall (_ : Mod (Exp b q) (Zpos xH) p) (_ : forall (d : nat) (_ : lt O d) (_ : Mod (Exp b d) (Zpos xH) p), le q d), le q (Init.Nat.pred p) *)
   elim H4. intros.
(* Goal: le q (Init.Nat.pred p) *)
   apply H6.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   apply lt_pred. assumption.
(* Goal: Mod (Exp b (Init.Nat.pred p)) (Zpos xH) p *)
   apply flt.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   assumption.
(* Goal: not (Mod b Z0 p) *)
   intro.
(* Goal: False *)
   elim (mod_0not1 p).
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   assumption.
(* Goal: Mod Z0 (Zpos xH) p *)
   apply mod_trans with (Exp b q).
(* Goal: Mod Z0 (Exp b q) p *)
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   apply mod_sym.
(* Goal: Mod (Exp b q) Z0 p *)
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   apply moda0_exp_compat.
(* Goal: gt p O *)
(* Goal: Mod b Z0 p *)
(* Goal: gt q O *)
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   unfold gt in |- *.
(* Goal: lt O p *)
(* Goal: Mod b Z0 p *)
(* Goal: gt q O *)
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   unfold gt in H1.
(* Goal: lt O p *)
(* Goal: Mod b Z0 p *)
(* Goal: gt q O *)
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   unfold lt in |- *.
(* Goal: le (S O) p *)
(* Goal: Mod b Z0 p *)
(* Goal: gt q O *)
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   apply lt_le_weak.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   assumption.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   assumption.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   assumption.
(* Goal: Mod (Exp b q) (Zpos xH) p *)
   assumption.
Qed.
