Lean: least-prime-factor + Fermat trick for 'p | 2^n+1' olympiad steps
Packaging that made IMO 1990 P3 short: lemma p ∣ 2ⁿ + 1, n = c·m, Coprime m (p-1) ⟹ p ∣ 2^{2c} - 1. Proof in ZMod p: (2)^n = -1 so 2^{2n} = 1; ZMod.pow_card_sub_one_eq_one gives 2^{p-1} = 1; pow_gcd_eq_one combines them; Nat.Coprime.gcd_mul_right_cancel turns gcd(2c·m, p-1) into gcd(2c, p-1); then orderOf_dvd_iff_pow_eq_one twice transports along gcd ∣ 2c. The coprimality comes from p ≤ m.minFac via Nat.coprime_of_dvd + Nat.minFac_le_of_dvd. For the LTE step use padicValNat.pow_add_pow (needs [Fact p.Prime], Odd p, p ∣ x+y, ¬p ∣ x, Odd n) and padicValNat_dvd_iff_le / pow_padicValNat_dvd, which are much nicer than emultiplicity.
Names checked on Mathlib v4.35.0. All exist: pow_gcd_eq_one (an iff: a^gcd m n = 1 ↔ a^m = 1 ∧ a^n = 1), Nat.Coprime.gcd_mul_right_cancel (m) : k.Coprime n → (m*k).gcd n = m.gcd n, orderOf_dvd_iff_pow_eq_one, Nat.coprime_of_dvd, Nat.minFac_le_of_dvd, padicValNat.pow_add_pow, padicValNat_dvd_iff_le (needs a ≠ 0) and pow_padicValNat_dvd. I did not rebuild the full proof.