From fe30314bc728339353a9a4e490c8aedc61287752 Mon Sep 17 00:00:00 2001
From: thery
Date: Wed, 10 Jul 2019 14:29:37 +0200
Subject: fermat little theorem

---
 CHANGELOG_UNRELEASED.md       |  2 ++
 mathcomp/ssreflect/binomial.v | 15 +++++++++++++++
 2 files changed, 17 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 55f44e6..ba58cb3 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -18,6 +18,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 - Added theorem `totient_prime` in `prime.v`
 
+- Added theorems `prime_modn_expSn` and `fermat_little` in `binomial.v`
+
 ### Changed
 
 - `eqVneq` lemma is changed from `{x = y} + {x != y}` to
diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v
index 06774ff..5896858 100644
--- a/mathcomp/ssreflect/binomial.v
+++ b/mathcomp/ssreflect/binomial.v
@@ -333,6 +333,21 @@ Proof.
 by apply/eqP; elim/big_rec2: _ => // i m n _; rewrite modnDml eqn_modDl.
 Qed.
 
+Lemma prime_modn_expSn p n : prime p -> n.+1 ^ p = (n ^ p).+1 %[mod p].
+Proof.
+case: p => // p pP.
+rewrite -[(_ ^ _).+1]addn0 (expnDn 1) big_ord_recr big_ord_recl /=.
+rewrite subnn binn exp1n !mul1n addnAC -modnDmr; congr ((_ + _) %% _).
+apply/eqP/dvdn_sum => -[i ?] _; exact/dvdn_mulr/prime_dvd_bin. 
+Qed. 
+
+Lemma fermat_little a p : prime p -> a ^ p = a %[mod p].
+Proof.
+move=> pP.
+elim: a => [|a IH]; first by rewrite exp0n // prime_gt0.
+by rewrite prime_modn_expSn // -addn1 -modnDml IH modnDml addn1.
+Qed.
+
 (* Combinatorial characterizations. *)
 
 Section Combinations.
-- 
cgit v1.2.3