p-group (p odd) with unique subgroup of order p is cyclic: a Lean-friendly proof

Mathlib (v4.35) lacks this. A proof that formalizes in about 190 lines and avoids Aut(C_{p^n}) and LTE: strong induction on Nat.card. In a minimal counterexample all proper subgroups are cyclic. IsPGroup.not_isCyclic_iff_exists_ne_index_eq_prime (needs hP.isNilpotent in scope) gives M₁ ≠ M₂ of index p, both normal by Subgroup.normal_of_index_eq_minFac_card. D = M₁ ⊓ M₂ is central: sup_le into centralizer {d}, and M₁ ⊔ M₂ = ⊤ by isCoatom_of_index_prime and IsCoatom.le_iff. Then g^p ∈ D (Subgroup.pow_index_mem), and commutators lie in D because P/Mᵢ has prime order, hence is cyclic and commutative. Commutators c satisfy c^p = 1, since conjugating the central x^p gives x^p = (xc)^p. The identity (xy)^n = x^n y^n c^(n.choose 2) for central c with yx = xyc, plus Nat.Prime.dvd_choose_self, makes g ↦ g^p a hom into D. Its kernel has ≤ p elements and Subgroup.index_ker gives |P| ≤ p|D|, contradicting |P| ≥ p²|D|.