proposition: Lemma pow : forall (a p:nat), Nprime p -> (p | (a+1)^p - a^p -1).
proof: Proof. intros. rewrite Nnewton. assert (exists p', p=S(S p')). destruct p. apply Nnot_prime_0 in H. contradiction. destruct p. apply Nnot_prime_1 in H. contradiction. exists p. reflexivity. destruct H0. rewrite H0. unfold Nnewton_sum. rewrite Nfinite_sum_split_lower. rewrite Nfinite_sum_split_upper. rewrite Nbinomial_0. rewrite Nbinomial_diag. rewrite Nat.mul_1_l. rewrite Nat.mul_1_l. rewrite Npower_1_n. rewrite Npower_1_n. rewrite Nat.mul_1_r. assert (1 + (Nfinite_sum_0_n x (fun k : nat => Nbinomial (S (S x)) (S k) * a ^ S k * 1 ^ (S (S x) - S k)) + a ^ S (S x)) - a ^ S (S x) - 1 = (Nfinite_sum_0_n x (fun k : nat => Nbinomial (S (S x)) (S k) * a ^ S k * 1 ^ (S (S x) - S k)) + 1 + a ^ S (S x)) - a ^ S (S x) - 1). rewrite Nat.add_assoc. auto with arith. rewrite H1. clear H1. rewrite plus_minus. rewrite Nat.sub_diag. rewrite Nat.add_0_r. rewrite plus_minus. rewrite Nat.sub_diag. rewrite Nat.add_0_r. rewrite <- H0. apply Nfinite_sum_div_compat. intros. apply Ndiv_mult_compat. apply Ndiv_mult_compat. apply Nbinomial_div. split. auto with arith. rewrite H0. auto with arith. auto. auto. auto. Qed.
imports: Coq(Arith Lia)