proposition: 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: Proof. intros. elim H0. intro. apply (lt_wf_ind x). intros X IH. intros. elim (exdec (fun m : nat => 0 < 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.
imports: Arith ZArith Wf_nat lemmas natZ dec list exp divides prime modulo modprime fermat