fact: 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).
imports: Arith ZArith Wf_nat lemmas natZ dec list exp divides prime modulo modprime fermat