proposition: Theorem Fermat's_little_theorem (p a : Z) : prime p -> ~(p | a) -> (p | a ^ (p - 1) - 1).
proof: Proof. assert (a = 0 \/ 0 < a \/ a < 0) as [ -> | [ pa | na ] ] by lia. - intros _ h; destruct h. apply Z.divide_0_r. - apply Fermat's_little_theorem_aux, pa. - intros pp pa. pose proof (Fermat's_little_theorem_aux p (- a) ltac:(lia) pp) as F. spec F. { intro h; apply pa. apply Zdivide_opp_r_rev in h. auto. } assert (p = 2 \/ p > 2) as [-> | p3] by now pose proof prime_ge_2 _ pp; lia. + rewrite <-Z.mod_divide in *; try lia. rewrite Zminus_mod, Zpow_mod. enough (a mod 2 = 1) as ->. reflexivity. pose proof Z.mod_pos_bound a 2. lia. + exact_eq F; do 2 f_equal. apply Z.pow_opp_even, Z.Odd_succ. enough (Z.Odd p) as h. exact_eq h. f_equal. lia. apply primes_are_often_odd. lia. auto. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz) Coqtail(Nlittle_fermat Ztools)