proposition: Lemma cent_core_acts_max_norm : [acts K, on |/|*(A; q) | 'JG].
proof: Proof. by rewrite (subset_trans _ (norm_acts_max_norm _ _)) ?cents_norm ?pcore_sub. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div choice fintype bigop) mathcomp(finset prime fingroup morphism automorphism action quotient) mathcomp(gfunctor cyclic pgroup center commutator gseries nilpotent) mathcomp(sylow abelian maximal hall) odd_order(BGsection1 BGsection6)