proposition: Lemma Fermat's_little_theorem_aux (p a : Z) : 0 < a -> prime p -> ~(p | a) -> (p | a ^ (p - 1) - 1).
proof: Proof. intros az pp pa. pose proof prime_ge_2 _ pp. pose proof Nlittle_fermat.Nlittle_fermat_alt2 (Z.to_nat a) (Z.to_nat p) as h. rewrite <-prime_Nprime in h. rewrite <-Zdivide_Ndivide in h; try lia. specialize (h pp pa). assert (0 <= a ^ (p - 1) - 1). { enough (1 <= a ^ (p - 1)) by lia. rewrite <-(Z.pow_1_l (p - 1)) at 1. 2:lia. apply Z.pow_le_mono_l. lia. } rewrite Zdivide_Ndivide; try lia. exact_eq h. f_equal. rewrite Z2Nat.inj_sub; try lia. rewrite Z2Nat_pow; try lia. do 2 f_equal. lia. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz) Coqtail(Nlittle_fermat Ztools)