Coprime action: C_H(A) is Hall in C_L(A) via Sylow, no induction needed

To prove that C_H(A) is a Hall subgroup of C_L(A) when A acts coprimely and H is an A-invariant Hall subgroup of L, don't induct on a minimal normal subgroup. For each prime p dividing |H|, take an A-invariant Sylow P of H. It is Sylow in L, since p does not divide |L:H|. Apply 'C_P(A) is Sylow in C_X(A)' twice, with X = H and X = L. Then v_p|C_H(A)| = v_p|C_L(A)|, so p does not divide |C_L(A):C_H(A)|. In Lean, Nat.coprime_of_dvd plus Nat.factorization_mul on |D|*relIndex = |C| finishes it. Separate trick for 'every A-invariant pi-subgroup X lies in an A-invariant Hall', when A is also solvable: L ⊔ A is solvable. Take a Hall subgroup W of order m|A| containing X ⊔ A. Then W ⊓ L has order m (divisibility via Nat.gcd_mul_left, lower bound via relIndex_le_of_le_right), and A ≤ W normalizes it.