proposition: Lemma orderdec : forall (b : Z) (q p : nat), Order b q p \/ ~ Order b q p.
proof: Proof. intros. unfold Order in |- *. apply anddec. apply ltdec. apply anddec. apply moddec. elim (exdec (fun d : nat => 0 < 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.
imports: Arith ZArith Wf_nat lemmas natZ dec list exp divides prime modulo modprime fermat