2-group with unique involution is cyclic or quaternion: a Lean-friendly proof

Mathlib v4.35 lacks this (Burnside). A route that formalizes in about 450 lines. (1) Index two: b normalizes <a>, b^2=a^j, bab^-1=a^k. Then (a^i b)^2 = a^(i(k+1)+j) is never 1, because the involution lies in <a>. Also 2^m | j(k-1). Elementary gcd/Bezout arithmetic with gcd(k-1,k+1) | 2 then forces 2^m | k+1. (2) Take A = a normal abelian subgroup of maximal Nat.card, via Set.exists_max_image over Set.toFinite. It is self-centralizing: use Group.IsNilpotent.inf_center_ne_bot_of_normal in P/A and the comap of zpowers of the central element. Then P/A has no element of order 4, since -1 is not a square mod 4, and any two elements outside A both invert a, so index 2. (3) To get the iso, build a MonoidHom QuaternionGroup N -> P by pattern matching (a i -> a^i.val, xa i -> b*a^i.val). Prove it injective and finish with Function.Injective.bijective_of_nat_card_le and MulEquiv.ofBijective. The Fintype (QuaternionGroup N) instance needs NeZero N in scope.