Replay Wolstenholme's theorem on current Lean

[DomTheDeveloper]

Purpose

Replays the exact historical proof of Wolstenholme's theorem:

p > 3 → p.Prime → (2*p - 1).choose (p - 1) ≡ 1 [MOD p^3]

The audit verifies immutable source blob a5f9775d0307b1dfff4cbc60cd25beb1f3a4ef90, builds the current catalog definitions, extracts only the theorem block, rejects holes and trust shortcuts, and audits the exact theorem footprint.

This is audit-only. If green, the current admitted textbook declaration can be queued for restoration.

[github-actions]

👋 This is an automated welcome message. 🤖
Thanks for the contributions!

A few friendly reminders while the review gets started:

• Please take a look at the style guidelines,
  especially the conventions for references, categories, AMS tags, and answer(sorry).
• You can manage some PR labels by leaving a comment with +label-name or -label-name; for example, +awaiting-author or -awaiting-author.
• This repository is mainly for formalised statements. Proofs longer than about 25-50 lines are usually out of scope; longer proofs are welcome to be included/linked via the formal_proof mechanism.

Thanks again for helping improve Formal Conjectures.