Grace/Cumulus/NumberTheory/Wilson.g17

Open in Workbench Download source

Imports

InverseInvolution · Nat.Subtraction

Declarations

Source

1-- Wilson's theorem: (p − 1)! ≡ −1 (mod p) for a prime p. The residues2-- 2, …, p − 2 pair off with their inverses, so their product is 1 mod p, and3-- the remaining factors 1 and p − 1 give −14-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.NumberTheory.Wilson10import InverseInvolution11import Nat.Subtraction1213-- Removing one occurrence of y keeps the product (after restoring y), keeps14-- every count (after restoring y), and drops the length by one.15predicate OneShorter (zs ys : Set) := length{ℕ}(ys) = succ(length{ℕ}(zs))1617predicate ShortList (xs k : Set) := length{ℕ}(xs) ≤ k1819theorem multiplicity.remove_length (y : Nat) (ys : List(ℕ))20  shows 0 < multiplicity(y, ys) →21    ∃ zs, List(ℕ, zs) ∧ ∏ ys = ∏ (y :: zs) ∧ OneShorter(zs, ys) ∧22      (∀ q, Nat(q) → multiplicity(q, ys) = multiplicity(q, y :: zs))23proof24  induction ys25  | List.nil =>26    intro positive27    have empty := multiplicity.nil at y28    rw empty at positive29    exfalso30    exact Less.irreflexive at 0 with *, positive31  | List.cons(x, rest) using ih =>32    intro positive33    have split : y = x ∨ ¬(y = x) by tauto34    cases split with equal | different35    . refine ⟨rest, h_rest, _, _, _⟩36      . rw equal37        rfl38      . unfold OneShorter39        exact length.cons with *40      . intros q qNat41        rw equal42        rfl43    . have restPositive : 0 < multiplicity(y, rest)44        have equation := multiplicity.cons_other with different45        rwa equation at positive46      obtain ⟨zs, zsList, product, lengths, counts⟩ := ih with restPositive47      have consList : List(ℕ, x :: zs) by typecheck48      refine ⟨x :: zs, consList, _, _, _⟩49      . have e1 := listProduct.cons at x, rest with *50        have e2 := listProduct.cons at y, zs with *51        have e3 := listProduct.cons at y, x :: zs with *52        have e4 := listProduct.cons at x, zs with *53        have zsProduct : Nat(∏ zs) by typecheck54        rw e2 at product55        rw [e1, e3, e4, product]56        ring57      . unfold OneShorter58        unfold OneShorter at lengths59        have l1 := length.cons at ℕ, x, rest with *60        have l2 := length.cons at ℕ, x, zs with *61        rw [l1, lengths, l2]62        rfl63      . intros q qNat64        have c1 := multiplicity.cons at q, x, rest with *65        have c2 := multiplicity.cons at q, y, x :: zs with *66        have c3 := multiplicity.cons at q, x, zs with *67        have c4 := multiplicity.cons at q, y, zs with *68        have count := counts with q, qNat69        rw c4 at count70        rw [c1, c2, c3, count]71        ring7273-- A list of distinct units mod p in which every entry's inverse is another74-- entry.75predicate Paired (p xs : Set) :=76  ∀ x, Nat(x) → 0 < multiplicity(x, xs) →77    (multiplicity(x, xs) = 1 ∧ 0 < x ∧ x < p ∧ modInverse(p, x) ≠ x ∧ 0 < multiplicity(modInverse(p, x), xs))7879-- The product of a paired list is 1 mod p.80theorem Paired.product (p k : Nat)81  requires prime : Prime(p)82  shows ∀ xs, List(ℕ, xs) → ShortList(xs, k) → Paired(p, xs) → (∏ xs) % p = 183proof84  induction k85  | zero =>86    intros xs xsList bound paired87    have aboveOne := Prime.greater_than_one with prime88    have shape := List.cases with xsList89    cases shape with nil | cons90    . rw [nil, listProduct.nil]91      exact mod.of_less with aboveOne92    . exfalso93      obtain ⟨x, xIn, rest, restList, equal⟩ := cons94      unfold ShortList at bound95      rw equal at bound96      have expand := length.cons at ℕ, x, rest with *97      rw expand at bound98      have lengthNat : Nat(length{ℕ}(rest)) by typecheck99      have impossible : ¬succ(length{ℕ}(rest)) ≤ 0 by arith100      exact impossible with bound101  | j + 1 using ih =>102    intros xs xsList bound paired103    have aboveOne := Prime.greater_than_one with prime104    have nonzero := Prime.nonzero with prime105    have shape := List.cases with xsList106    cases shape with nil | cons107    . rw [nil, listProduct.nil]108      exact mod.of_less with aboveOne109    . obtain ⟨x, xIn, rest, restList, equal⟩ := cons110      have xNat : Nat(x) by typecheck111      unfold ShortList at bound112      rw equal at bound113      rw equal at paired114      rw equal115      unfold Paired at paired116      have xPositive : 0 < multiplicity(x, x :: rest)117        have self := multiplicity.cons_self at x, rest with *118        rw self119        arith120      obtain ⟨once, xPos, xBelow, notFixed, inverseIn⟩ := paired with x, xNat, xPositive121      have unit := prime.coprime_below with prime, xPos, xBelow122      have yNat := modInverse.natural with prime, unit123      have yBelow := modInverse.below with prime, unit124      have yPos := modInverse.positive with prime, unit125      have yUnit := modInverse.unit with prime, unit126      have product := modInverse.product with prime, unit127      have involution := modInverse.involution with prime, unit, xBelow128      have restZero : multiplicity(x, rest) = 0129        have self := multiplicity.cons_self at x, rest with *130        rw self at once131        have shifted : 1 + multiplicity(x, rest) = 1 + 0132          have zeroForm : 1 + 0 = (1:N) by ring133          rwa zeroForm134        have cancel := add.left_cancel at multiplicity(x, rest), 0, 1135        exact cancel with shifted136      have yInRest : 0 < multiplicity(modInverse(p, x), rest)137        have other := multiplicity.cons_other at modInverse(p, x), x, rest with notFixed138        rwa other at inverseIn139      have remove := multiplicity.remove_length at modInverse(p, x), rest with *140      obtain ⟨zs, zsList, productRest, lengthRest, counts⟩ := remove with yInRest141      have lengthZs : ShortList(zs, j)142        unfold ShortList143        unfold OneShorter at lengthRest144        have expand := length.cons at ℕ, x, rest with *145        rw [expand, lengthRest] at bound146        have zsLengthNat : Nat(length{ℕ}(zs)) by typecheck147        arith148      have yOnce : multiplicity(modInverse(p, x), x :: rest) = 1149        have propsY := paired with modInverse(p, x), inverseIn150        exact propsY.left151      have yZero : multiplicity(modInverse(p, x), zs) = 0152        have other := multiplicity.cons_other at modInverse(p, x), x, rest with notFixed153        have count := counts with modInverse(p, x)154        have self := multiplicity.cons_self at modInverse(p, x), zs with *155        rw [other, count, self] at yOnce156        have shifted : 1 + multiplicity(modInverse(p, x), zs) = 1 + 0157          have zeroForm : 1 + 0 = (1:N) by ring158          rwa zeroForm159        have cancel := add.left_cancel at multiplicity(modInverse(p, x), zs), 0, 1160        exact cancel with shifted161      have pairedZs : Paired(p, zs)162        unfold Paired163        intros q qNat qPositive164        have countQ := counts with q, qNat165        have consQ := multiplicity.cons at q, modInverse(p, x), zs with *166        have weightNat := chooseNat.natural at equalNat(q, modInverse(p, x)), 1, 0167        have qInRest : 0 < multiplicity(q, rest)168          rw [countQ, consQ]169          arith170        have qInXs := multiplicity.positive_cons at q, x, rest with qInRest171        obtain ⟨onceQ, qPos, qBelow, qNotFixed, qInverseIn⟩ := paired with q, qNat, qInXs172        have qUnit := prime.coprime_below with prime, qPos, qBelow173        have rNat := modInverse.natural with prime, qUnit174        have qInvolution := modInverse.involution with prime, qUnit, qBelow175        have qNotX : q ≠ x176          intro same177          rw [same, restZero] at qInRest178          exact Less.irreflexive with *, qInRest179        have qNotY : q ≠ modInverse(p, x)180          intro same181          rw [same, yZero] at qPositive182          exact Less.irreflexive with *, qPositive183        constructor184        . have consX := multiplicity.cons_other at q, x, rest with qNotX185          rw consX at onceQ186          rw [countQ, consQ] at onceQ187          have otherY := equalNat.false_iff.backward with qNotY188          rw otherY at onceQ189          have weightZero : chooseNat(Bool.false, 1, 0) = 0 by compute190          rw weightZero at onceQ191          have zeroForm : 0 + multiplicity(q, zs) = multiplicity(q, zs) by ring192          rwa zeroForm at onceQ193        . constructor194          . exact qPos195          . constructor196            . exact qBelow197            . constructor198              . exact qNotFixed199              . have rNotX : modInverse(p, q) ≠ x200                  intro same201                  apply qNotY202                  rw [← qInvolution, same]203                  rfl204                have rNotY : modInverse(p, q) ≠ modInverse(p, x)205                  intro same206                  apply qNotX207                  rw ← qInvolution208                  rw [same, involution]209                  rfl210                have countR := counts with modInverse(p, q)211                have consRX := multiplicity.cons_other at modInverse(p, q), x, rest with rNotX212                have consRY := multiplicity.cons_other at modInverse(p, q), modInverse(p, x), zs with rNotY213                rw consRX at qInverseIn214                rwa [countR, consRY] at qInverseIn215      have previous := ih with zs, zsList, lengthZs, pairedZs216      have expandXs := listProduct.cons at x, rest with *217      have expandRest := listProduct.cons at modInverse(p, x), zs with *218      have zsProduct : Nat(∏ zs) by typecheck219      rw expandRest at productRest220      have rearrange := mul.associative_reverse at modInverse(p, x), ∏ zs, x with *221      have split := mod.mul at p, x * modInverse(p, x), ∏ zs with nonzero222      have oneSelf := mod.of_less with aboveOne223      have oneOne : (1:N) * 1 = 1 by ring224      rwa [expandXs, productRest, rearrange, split, product, previous, oneOne]225226-- The list p − 1, …, 1 and its product.227def factorialList (m : Nat) → List(ℕ)228  | zero => []229  | succ(k) => succ(k) :: factorialList(k)230231theorem factorialList.zero232  shows factorialList(0) = []233proof234  compute235236theorem factorialList.succ (k : Nat)237  shows factorialList(succ(k)) = succ(k) :: factorialList(k)238proof239  simp [factorialList]240241theorem factorialList.list (m : Nat)242  shows List(ℕ, factorialList(m))243proof244  induction m245  | zero =>246    rw factorialList.zero247    typecheck248  | succ(k) using ih =>249    rw factorialList.succ250    typecheck251252theorem factorialList.product (m : Nat)253  shows ∏ factorialList(m) = m!254proof255  induction m256  | zero =>257    rw [factorialList.zero, listProduct.nil]258    compute259  | succ(k) using ih =>260    have restList := factorialList.list at k261    have expand := listProduct.cons at succ(k), factorialList(k) with *262    have step : succ(k)! = succ(k) * k!263      simp [factorial]264    rw [factorialList.succ, expand, ih, step]265    rfl266267-- The list k + 1, …, 2, the residues strictly between 1 and p − 1 when268-- p = k + 3.269def middleList (k : Nat) → List(ℕ)270  | zero => []271  | succ(j) => succ(succ(j)) :: middleList(j)272273theorem middleList.zero274  shows middleList(0) = []275proof276  compute277278theorem middleList.succ (j : Nat)279  shows middleList(succ(j)) = succ(succ(j)) :: middleList(j)280proof281  simp [middleList]282283theorem middleList.list (k : Nat)284  shows List(ℕ, middleList(k))285proof286  induction k287  | zero =>288    rw middleList.zero289    typecheck290  | succ(j) using ih =>291    rw middleList.succ292    typecheck293294theorem middleList.product (k : Nat)295  shows ∏ factorialList(succ(k)) = ∏ middleList(k)296proof297  induction k298  | zero =>299    have expand := listProduct.cons at succ(0), factorialList(0) with *300    rw [factorialList.succ, expand, factorialList.zero, listProduct.nil, middleList.zero, listProduct.nil]301    compute302  | succ(j) using ih =>303    have restList := factorialList.list at succ(j)304    have middleRest := middleList.list at j305    have expandFactorial := listProduct.cons at succ(succ(j)), factorialList(succ(j)) with *306    have expandMiddle := listProduct.cons at succ(succ(j)), middleList(j) with *307    rw [factorialList.succ, expandFactorial, ih, middleList.succ, expandMiddle]308    rfl309310theorem middleList.multiplicity_out (k x : Nat)311  requires outside : ¬(2 ≤ x ∧ x ≤ succ(k))312  shows multiplicity(x, middleList(k)) = 0313proof314  induction k315  | zero =>316    intro outside317    rw middleList.zero318    exact multiplicity.nil at x319  | succ(j) using ih =>320    intro outside321    have middleRest := middleList.list at j322    have different : x ≠ succ(succ(j))323      intro same324      apply outside325      rw same326      constructor327      . arith328      . arith329    have smaller : ¬(2 ≤ x ∧ x ≤ succ(j))330      intro both331      obtain ⟨lower, upper⟩ := both332      apply outside333      constructor334      . exact lower335      . arith336    have previous := ih with smaller337    have other := multiplicity.cons_other at x, succ(succ(j)), middleList(j) with different338    rw [middleList.succ, other]339    exact previous340341theorem middleList.multiplicity_in (k x : Nat)342  requires lower : 2 ≤ x343  requires upper : x ≤ succ(k)344  shows multiplicity(x, middleList(k)) = 1345proof346  induction k347  | zero =>348    intro upper349    exfalso350    have impossible : ¬x ≤ succ(0) by arith351    exact impossible with upper352  | succ(j) using ih =>353    intro upper354    have middleRest := middleList.list at j355    have trichotomy := Less.trichotomy at x, succ(succ(j))356    rcases trichotomy with below | same | above357    . have smaller : x ≤ succ(j) by arith358      have previous := ih with smaller359      have different : x ≠ succ(succ(j))360        intro equal361        rw equal at below362        exact Less.irreflexive at succ(succ(j)) with *, below363      have other := multiplicity.cons_other at x, succ(succ(j)), middleList(j) with different364      rw [middleList.succ, other]365      exact previous366    . have outside : ¬(2 ≤ x ∧ x ≤ succ(j))367        intro both368        obtain ⟨lowerX, upperX⟩ := both369        rw same at upperX370        have impossible : ¬succ(succ(j)) ≤ succ(j) by arith371        exact impossible with upperX372      have zero := middleList.multiplicity_out at j, x with outside373      rw middleList.succ374      rw same375      have self := multiplicity.cons_self at succ(succ(j)), middleList(j) with *376      rw self377      rw same at zero378      rw zero379      ring380    . exfalso381      have impossible : ¬succ(succ(j)) < x by arith382      exact impossible with above383384theorem middleList.member (k x : Nat)385  requires positive : 0 < multiplicity(x, middleList(k))386  shows 2 ≤ x ∧ x ≤ succ(k)387proof388  by_contra none389  have zero := middleList.multiplicity_out with none390  rw zero at positive391  exact Less.irreflexive with *, positive392393-- p − 1 is its own inverse.394theorem modInverse.top (k : Nat)395  requires prime : Prime(succ(succ(succ(k))))396  shows modInverse(succ(succ(succ(k))), succ(succ(k))) = succ(succ(k))397proof398  have nonzero := Prime.nonzero at succ(succ(succ(k))) with prime399  have positive : 0 < succ(succ(k)) by arith400  have below : succ(succ(k)) < succ(succ(succ(k))) by arith401  have unit := prime.coprime_below at succ(succ(succ(k))), succ(succ(k)) with prime, positive, below402  have square : succ(succ(k)) * succ(succ(k)) = succ(succ(succ(k))) * succ(k) + 1 by ring403  have oneBelow : 1 < succ(succ(succ(k))) by arith404  have product : (succ(succ(k)) * succ(succ(k))) % succ(succ(succ(k))) = 1405    rw square406    have shifted := mod.add_multiple at succ(succ(succ(k))), 1, succ(k) with nonzero407    have commute : succ(succ(succ(k))) * succ(k) + 1 = 1 + succ(succ(succ(k))) * succ(k) by ring408    rw [commute, shifted]409    exact mod.of_less at succ(succ(succ(k))), 1 with oneBelow410  have same := modInverse.unique_below at succ(succ(succ(k))), succ(succ(k)), succ(succ(k)) with prime, unit, below, product411  symm at same412  exact same413414theorem middleList.paired (k : Nat)415  requires prime : Prime(succ(succ(succ(k))))416  shows Paired(succ(succ(succ(k))), middleList(k))417proof418  unfold Paired419  intros x xNat positive420  obtain ⟨lower, upper⟩ := middleList.member at k, x with positive421  have xPos : 0 < x by arith422  have xBelow : x < succ(succ(succ(k))) by arith423  have unit := prime.coprime_below with prime, xPos, xBelow424  have yNat := modInverse.natural with prime, unit425  have yPos := modInverse.positive with prime, unit426  have yBelow := modInverse.below with prime, unit427  have product := modInverse.product with prime, unit428  have involution := modInverse.involution with prime, unit, xBelow429  have nonzero := Prime.nonzero with prime430  have notFixed : modInverse(succ(succ(succ(k))), x) ≠ x431    intro fixed432    have cases := modInverse.fixed with prime, xPos, xBelow, fixed433    cases cases with one | top434    . rw one at lower435      have impossible : ¬(2:N) ≤ 1 by arith436      exact impossible with lower437    . have impossible : succ(x) ≠ succ(succ(succ(k))) by arith438      exact impossible with top439  have yNotOne : modInverse(succ(succ(succ(k))), x) ≠ 1440    intro one441    rw one at product442    have same : mul(x, 1) = x by ring443    rw same at product444    have self := mod.of_less with xBelow445    rw self at product446    rw product at lower447    have impossible : ¬(2:N) ≤ 1 by arith448    exact impossible with lower449  have yNotTop : modInverse(succ(succ(succ(k))), x) ≠ succ(succ(k))450    intro top451    have topInverse := modInverse.top with prime452    have same : x = succ(succ(k))453      rw ← involution454      rw [top, topInverse]455      rfl456    rw same at upper457    have impossible : ¬succ(succ(k)) ≤ succ(k) by arith458    exact impossible with upper459  have yLower : 2 ≤ modInverse(succ(succ(succ(k))), x)460    have trichotomy := Less.trichotomy at modInverse(succ(succ(succ(k))), x), 2461    rcases trichotomy with below | same | above462    . exfalso463      have atMostOne : modInverse(succ(succ(succ(k))), x) ≤ 1 by arith464      have oneLe : 1 ≤ modInverse(succ(succ(succ(k))), x) by arith465      have equal := LessEqual.antisymmetric with atMostOne, oneLe466      exact yNotOne with equal467    . rw same468      arith469    . arith470  have yUpper : modInverse(succ(succ(succ(k))), x) ≤ succ(k)471    have atMost : modInverse(succ(succ(succ(k))), x) ≤ succ(succ(k)) by arith472    have trichotomy := Less.trichotomy at modInverse(succ(succ(succ(k))), x), succ(succ(k))473    rcases trichotomy with below | same | above474    . arith475    . exfalso476      exact yNotTop with same477    . exfalso478      have impossible : ¬succ(succ(k)) < modInverse(succ(succ(succ(k))), x) by arith479      exact impossible with above480  have once := middleList.multiplicity_in with lower, upper481  have yIn := middleList.multiplicity_in with yLower, yUpper482  constructor483  . exact once484  . constructor485    . exact xPos486    . constructor487      . exact xBelow488      . constructor489        . exact notFixed490        . rw yIn491          arith492493-- Wilson's theorem.494theorem wilson.theorem (p : Nat)495  requires prime : Prime(p)496  shows ((p - 1)! + 1) % p = 0497proof498  have aboveOne := Prime.greater_than_one with prime499  have nonzero := Prime.nonzero with prime500  have shape := natural.zero_or_successor at p501  cases shape with zero | successor502  . exfalso503    exact nonzero with zero504  . obtain ⟨q, qNat, form⟩ := successor505    have qShape := natural.zero_or_successor at q506    cases qShape with qZero | qSuccessor507    . exfalso508      rw [form, qZero] at aboveOne509      exact Less.irreflexive with *, aboveOne510    . obtain ⟨r, rNat, qForm⟩ := qSuccessor511      have rShape := natural.zero_or_successor at r512      cases rShape with rZero | rSuccessor513      . rw [form, qForm, rZero]514        compute515      . obtain ⟨k, kNat, rForm⟩ := rSuccessor516        have pForm : p = succ(succ(succ(k)))517          rw [form, qForm, rForm]518          rfl519        rw pForm520        rw pForm at prime521        have predecessorValue : succ(succ(succ(k))) - 1 = succ(succ(k)) by simp [sub, predecessor]522        rw predecessorValue523        have factorialValue := factorialList.product at succ(succ(k))524        have middleList2 := middleList.list at k525        have factorialRest := factorialList.list at succ(k)526        have expand := listProduct.cons at succ(succ(k)), factorialList(succ(k)) with *527        have middle := middleList.product at k528        have paired := middleList.paired with prime529        have products := Paired.product at succ(succ(succ(k))), length{ℕ}(middleList(k)) with prime530        have lengthNat : Nat(length{ℕ}(middleList(k))) by typecheck531        have reflexive : ShortList(middleList(k), length{ℕ}(middleList(k)))532          unfold ShortList533          witness 0534          ring535        have middleProduct := products with middleList(k), middleList2, reflexive, paired536        have middleNat : Nat(∏ middleList(k)) by typecheck537        have pNonzero : succ(succ(succ(k))) ≠ 0 by arith538        have factorialForm : succ(succ(k))! = succ(succ(k)) * ∏ middleList(k)539          rw [← factorialValue, factorialList.succ, expand, middle]540          rfl541        rw factorialForm542        have addMod := mod.add at succ(succ(succ(k))), succ(succ(k)) * ∏ middleList(k), 1 with pNonzero543        have mulMod := mod.mul_right at succ(succ(succ(k))), succ(succ(k)), ∏ middleList(k) with pNonzero544        have topBelow : succ(succ(k)) < succ(succ(succ(k))) by arith545        have oneBelow : 1 < succ(succ(succ(k))) by arith546        have topSelf := mod.of_less with topBelow547        have oneSelf := mod.of_less with oneBelow548        have topOne : succ(succ(k)) * 1 = succ(succ(k)) by ring549        rw [addMod, ← mulMod, middleProduct, topOne, topSelf, oneSelf]550        have full : succ(succ(k)) + 1 = succ(succ(succ(k))) * 1 + 0 by ring551        rw full552        have zeroBelow : 0 < succ(succ(succ(k))) by arith553        have equation : succ(succ(succ(k))) * 1 + 0 = succ(succ(succ(k))) * 1 + 0 by rfl554        exact mod.unique with pNonzero, equation, zeroBelow555556-- The converse: a natural number above one that divides (n - 1)! + 1 is557-- prime, since any proper divisor d of n also divides (n - 1)! and hence 1.558theorem wilson.converse (n : Nat)559  requires aboveOne : 1 < n560  requires congruence : ((n - 1)! + 1) % n = 0561  shows Prime(n)562proof563  have nonzero : n ≠ 0 by arith564  have dividesSum : n ∣ (n - 1)! + 1565    have characterization := mod.zero_iff at n, (n - 1)! + 1 with nonzero566    exact characterization.forward with congruence567  have shape := natural.zero_or_successor at n568  cases shape with zero | successor569  . exfalso570    exact nonzero with zero571  obtain ⟨k, kNat, form⟩ := successor572  have predecessorForm : n - 1 = k573    rw [form, sub.one, predecessor.succ]574    rfl575  rw predecessorForm at dividesSum576  unfold Prime577  constructor578  . have oneMember := membership.of_Less at 1, n with *579    exact oneMember with aboveOne580  . intros d dNat dBelow dDivides581    have dNonzero : d ≠ 0582      intro dZero583      rw dZero at dDivides584      have nZero := zero.divides_only_zero at n with dDivides585      exact nonzero with nZero586    have dShape := natural.zero_or_successor at d with dNat587    cases dShape with dZero | dSuccessor588    . exfalso589      exact dNonzero with dZero590    obtain ⟨j, jNat, dForm⟩ := dSuccessor591    have dPositiveLess : 0 < d592      rw dForm593      arith594    have dPositive := membership.of_Less at 0, d with *, *, dPositiveLess595    rw form at dBelow596    have through := factorial.divisible_through at d, k with dNat597    have dividesFactorial := through with dPositive, dBelow598    have dividesPlus := divides.transitive at d, n, k! + 1 with dDivides, dividesSum599    have dividesOne := divides.add_cancel_left at d, k!, 1 with dividesFactorial, dividesPlus600    exact divides.one_only at d with dNat, dividesOne601602theorem wilson.characterization (n : Nat)603  requires aboveOne : 1 < n604  shows Prime(n) ↔ ((n - 1)! + 1) % n = 0605proof606  constructor607  . intro prime608    exact wilson.theorem with prime609  . intro congruence610    exact wilson.converse with aboveOne, congruence611