proposition: Theorem Nlittle_fermat : forall a p, Nprime p -> (p | a ^ p - a).
proof: Proof. induction a. intros. rewrite Npower_0_n. simpl. apply Ndiv_0. destruct p. apply Nnot_prime_0 in H. contradiction. destruct p. apply Nnot_prime_1 in H. contradiction. auto with arith. intros. destruct p. apply Nnot_prime_0 in H. contradiction. destruct p. apply Nnot_prime_1 in H. contradiction. simpl. replace (S a) with (a+1). replace ((a+1)^(S(S p))-(a+1)) with ((a+1)^(S(S p))-a-1). assert((S(S p))|(a+1)^(S(S p)) - a^(S (S p))-1). apply pow. auto. assert((S(S p))|((a+1)^(S(S p))-a^(S(S p))-1)+(a^(S(S p))-a)). apply Ndiv_plus_compat. auto. apply IHa. auto. clear H0. assert((a + 1) ^ S (S p) - a ^ S (S p) - 1 + (a ^ S (S p) - a) =(a + 1) ^ S (S p) - a - 1). assert((a+1)^(S(S p))>=a^(S(S p))+1). assert((a+1)^(S(S p))>=a^(S(S p))+1^(S (S p))). apply Npower_plus_le_compat. auto with arith. rewrite Npower_1_n in H0. auto. apply Nle_plus in H0. destruct H0. rewrite H0. clear H0. rewrite minus_L0. rewrite (Nat.add_comm (a ^ _)) at 1. rewrite Nat.add_sub. rewrite (Nat.add_comm 1). rewrite Nat.add_sub. replace (a ^ S (S p) + 1 + x - a - 1) with (1+(a ^ S (S p) + x - a) - 1). symmetry. rewrite (Nat.add_comm 1). symmetry. rewrite Nat.add_sub. rewrite minus_L1. auto with arith. destruct a. rewrite Npower_0_n. auto. auto with arith. apply Nat.le_trans with ((S a)^1). rewrite Npower_n_1. auto. apply Npower_le_compat_r. auto with arith. auto with arith. rewrite minus_L1. rewrite Nat.add_assoc. auto with arith. destruct a. rewrite Npower_0_n. simpl. auto with arith. auto with arith. apply Nat.le_trans with ((S a)^(S(S p))). apply Nat.le_trans with ((S a)^1). rewrite Npower_n_1. auto. apply Npower_le_compat_r. auto with arith. auto with arith. auto with arith. auto with arith. rewrite H0 in H1. revert H1; match goal with |- (?a | ?b) -> (?a | ?c) => cut (b = c) end. now intros ->. replace (a + 1) with (1 + a) by ring; simpl. repeat rewrite <- Nat.add_assoc. lia. lia. lia. Qed.
imports: Coq(Arith Lia)