Wikipedia/Mersenne: prove `new_mersenne_conjecture_of_prime`

[ChakshuGupta13]

In FormalConjectures/Wikipedia/Mersenne.lean, the textbook reduction

@[category textbook, AMS 11]
theorem new_mersenne_conjecture_of_prime :
    (∀ p, p.Prime → NewMersenneConjectureStatement p) →
    ∀ p, Odd p → NewMersenneConjectureStatement p

says that it suffices to verify the New Mersenne Conjecture at prime exponents: the three biconditional implications hold for every odd p as soon as they hold for every prime p.

The reduction is the standard folklore argument. For odd composite p:

• (mersenne p).Prime is false because Mathlib.NumberTheory.LucasLehmer already provides Nat.Prime.of_mersenne : (mersenne p).Prime → Nat.Prime p, so the contrapositive applies.
• p.GivesWagstaffPrime is false because (2^p + 1)/3 admits a proper divisor: let q := p.minFac (an odd prime with 3 ≤ q < p) and s := p / q. Then Odd.nat_add_dvd_pow_add_pow yields (2^q + 1) ∣ (2^p + 1), and a short ZMod 3 computation gives 3 ∣ 2^q + 1 for odd q. Dividing by 3 on both sides produces a divisor (2^q+1)/3 of (2^p+1)/3 strictly between 3 and (2^p+1)/3.

With both antecedents false, all three implications hold vacuously and the prime case discharges via the hypothesis.

I have a working proof (~85 lines, two small private auxiliary lemmas + a by_cases on p.Prime in the main theorem) and will open a PR.