proposition: Lemma order_ex : forall (b : Z) (p : nat), Prime p -> ~ Mod b 0 p -> exists x : nat, x < p /\ Order b x p.
proof: 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 flt. 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 flt. assumption. assumption. Qed.
imports: Arith ZArith Wf_nat lemmas natZ dec list exp divides prime modulo modprime fermat