proposition: Theorem Wilson p : p > 1 -> prime p = (p %| ((p.-1)`!).+1).
proof: Proof. have dFact n: 0 < n -> (n.-1)`! = \prod_(0 <= i < n | i != 0) i. move=> n_gt0; rewrite -big_filter fact_prod; symmetry; apply: congr_big => //. rewrite /index_iota subn1 -[n]prednK //=; apply/all_filterP. by rewrite all_predC has_pred1 mem_iota. move=> lt1p; have p_gt0 := ltnW lt1p. apply/idP/idP=> [pr_p | dv_pF]; last first. apply/primeP; split=> // d dv_dp; have: d <= p by apply: dvdn_leq. rewrite orbC leq_eqVlt => /orP[-> // | ltdp]. have:= dvdn_trans dv_dp dv_pF; rewrite dFact // big_mkord. rewrite (bigD1 (Ordinal ltdp)) /=; last by rewrite -lt0n (dvdn_gt0 p_gt0). by rewrite orbC -addn1 dvdn_addr ?dvdn_mulr // dvdn1 => ->. pose Fp1 := Ordinal lt1p; pose Fp0 := Ordinal p_gt0. have ltp1p: p.-1 < p by [rewrite prednK]; pose Fpn1 := Ordinal ltp1p. case eqF1n1: (Fp1 == Fpn1); first by rewrite -{1}[p]prednK -1?((1 =P p.-1) _). have toFpP m: m %% p < p by rewrite ltn_mod. pose toFp := Ordinal (toFpP _); pose mFp (i j : 'I_p) := toFp (i * j). have Fp_mod (i : 'I_p) : i %% p = i by apply: modn_small. have mFpA: associative mFp. by move=> i j k; apply: val_inj; rewrite /= modnMml modnMmr mulnA. have mFpC: commutative mFp by move=> i j; apply: val_inj; rewrite /= mulnC. have mFp1: left_id Fp1 mFp by move=> i; apply: val_inj; rewrite /= mul1n. have mFp1r: right_id Fp1 mFp by move=> i; apply: val_inj; rewrite /= muln1. pose mFpcM := Monoid.isComLaw.Build 'I_p Fp1 mFp mFpA mFpC mFp1. pose mFpCL : Monoid.com_law _ := HB.pack mFp mFpcM. pose mFpM := Monoid.Law.sort mFpCL. pose vFp (i : 'I_p) := toFp (egcdn i p).1. have vFpV i: i != Fp0 -> mFp (vFp i) i = Fp1. rewrite -val_eqE /= -lt0n => i_gt0; apply: val_inj => /=. rewrite modnMml; case: egcdnP => //= _ km -> _; rewrite {km}modnMDl. suffices: coprime i p by move/eqnP->; rewrite modn_small. rewrite coprime_sym prime_coprime //; apply/negP=> /(dvdn_leq i_gt0). by rewrite leqNgt ltn_ord. have vFp0 i: i != Fp0 -> vFp i != Fp0. by move/vFpV; apply/contra_eq_neq => ->; rewrite -val_eqE /= mul0n mod0n. have vFpK: {in predC1 Fp0, involutive vFp}. move=> i n0i; rewrite /= -[vFp _]mFp1r -(vFpV _ n0i) mFpA. by rewrite vFpV (vFp0, mFp1). have le_pmFp (i : 'I_p) m: i <= p + m. by apply: leq_trans (ltnW _) (leq_addr _ _). have eqFp (i j : 'I_p): (i == j) = (p %| p + i - j). by rewrite -eqn_mod_dvd ?(modnDl, Fp_mod). have vFpId i: (vFp i == i :> nat) = xpred2 Fp1 Fpn1 i. have [->{i} | ni0] := eqVneq i Fp0. by rewrite -!val_eqE /= egcd0n modn_small //= -(subnKC lt1p). rewrite 2!eqFp -Euclid_dvdM // -[_ - p.-1]subSS prednK //. have lt0i: 0 < i by rewrite lt0n. rewrite -addnS addKn -addnBA // mulnDl -{2}(addn1 i) -subn_sqr. rewrite addnBA ?leq_sqr // mulnS -addnA -mulnn -mulnDl. rewrite -(subnK (le_pmFp (vFp i) i)) mulnDl addnCA. rewrite -[1 ^ 2]/(Fp1 : nat) -addnBA // dvdn_addl. by rewrite Euclid_dvdM // -eqFp eq_sym orbC /dvdn Fp_mod eqn0Ngt lt0i. by rewrite -eqn_mod_dvd // Fp_mod modnDl -(vFpV _ ni0). suffices [mod_fact]: toFp (p.-1)`! = Fpn1. by rewrite /dvdn -addn1 -modnDml mod_fact addn1 prednK // modnn. rewrite dFact //; rewrite ((big_morph toFp) Fp1 mFpM) //; first last. - by apply: val_inj; rewrite /= modn_small. - by move=> i j; apply: val_inj; rewrite /= modnMm. rewrite big_mkord (eq_bigr id) => [|i _]; last by apply: val_inj => /=. pose ltv i := vFp i < i; rewrite (bigID ltv) -/mFpM [mFpM _ _]mFpC. rewrite (bigD1 Fp1) -/mFpM; last by rewrite [ltv _]ltn_neqAle vFpId. rewrite [mFpM _ _]mFp1 (bigD1 Fpn1) -?mFpA -/mFpM; last first. rewrite -lt0n -ltnS prednK // lt1p. by rewrite [ltv _]ltn_neqAle vFpId eqxx orbT eq_sym eqF1n1. rewrite (reindex_onto vFp vFp) -/mFpM => [|i]; last by do 3!case/andP; auto. rewrite (eq_bigl (xpredD1 ltv Fp0)) => [|i]; last first. rewrite andbC -!andbA -2!negb_or -vFpId orbC -leq_eqVlt -ltnNge. have [->|ni0] := eqVneq i; last by rewrite vFpK // eqxx vFp0. by case: eqP => // ->; rewrite !andbF. rewrite -{2}[mFp]/mFpM -[mFpM _ _]big_split -/mFpM. by rewrite big1 ?mFp1r //= => i /andP [/vFpV]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)