Require Import Arith.
Require Export Nnewton.
Require Export Ndiv.
Open Scope nat_scope.

Theorem Nlittle_fermat :
  ∀ a p, Nprime p → (p | a ^ p - a).

Theorem Nlittle_fermat_alt :
  ∀ a p, Nprime p → Nrel_prime a p →
  (p | a ^ (pred p) - 1).
Proof.
intros.
destruct p.
apply Nnot_prime_0 in H. contradiction.
destruct p.
apply Nnot_prime_1 in H. contradiction.
assert(S(S p)|a^(S(S p))-a).
apply Nlittle_fermat.
auto.
simpl.
rewrite Npower_succ in H1.
replace (a × a ^ S p - a) with (a × a ^ S p - a×1) in H1.
rewrite <- mult_minus_distr_l in H1.
apply Ngauss in H1.
auto.
apply Nrel_prime_comm. auto.
rewrite mult_1_r.
auto.
Qed.