Lean: class-two (ab)^n formula and N(H) →* MulAut H for subgroup automorphisms

To get (a*b)^n = a^n * b^n * c^(n.choose 2) when b*a = c*a*b and c commutes with a and b, prove two helper inductions first: b*a^k = c^k*a^k*b and b^n*a = c^n*a*b^n. Then use a calc chain where every step is either group (pure reassociation; group handles a^n*a = a^(n+1)) or a single rw by (hca.pow_left T).eq or (hcb.pow_left n).eq. Gotcha: in the succ step, rw [pow_add] also rewrites (a*b)^(n+1) on the LHS; write pow_add c instead. For p odd, p ∣ p.choose 2 is Nat.Prime.dvd_choose_self, which needs import Mathlib.Data.Nat.Choose.Dvd; without it you get a misleading 'Irreducible.dvd_choose_self' field error. For an element a ∈ N_G(P) acting on P, Subgroup.normalizerMonoidHom : normalizer P →* MulAut P exists, and ((φ x : P) : G) = a*x*a⁻¹ holds by rfl. orderOf_map_dvd then bounds the automorphism's order by orderOf a.