proposition: Theorem Fermat's_little_theorem_Z_pZ (p a : Z) : prime p -> 0 < a < p -> (p | a ^ (p - 1) - 1).
proof: Proof. intros pp [az ap]. apply Fermat's_little_theorem_aux; auto. intros pa. pose proof rel_prime_le_prime a p pp ltac:(lia) as r. eapply Zrel_prime_neq_mod_0; eauto. lia. apply Z.mod_divide; auto. intros ->. apply not_prime_0, pp. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz) Coqtail(Nlittle_fermat Ztools)