proposition: Lemma Frobenius_cent1_ker : {in K^#, forall x, 'C_G[x] \subset K}.
proof: Proof. have [/eqP defG _ /normedTI_memJ_P[_ _ tiHG]] := and3P frobG. move=> x /setD1P[ntx Kx]; have [_ /mulG_sub[sKG _] _ tiKH] := sdprodP defG. have [/eqP <- _ _] := and3P Frobenius_partition; rewrite big_distrl /=. apply/bigcupsP=> _ /setU1P[|/imsetP[y Ky]] ->; first exact: subsetIl. apply: contraR ntx => /subsetPn[z]; rewrite inE mem_conjg => /andP[Hzy cxz] _. rewrite -(conjg_eq1 x y^-1) -in_set1 -set1gE -tiKH inE andbC. rewrite -(tiHG _ _ Hzy) ?(subsetP sKG) ?in_group // Ky andbT -conjJg. by rewrite /(z ^ x) (cent1P cxz) mulKg. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div) mathcomp(fintype bigop prime finset fingroup morphism) mathcomp(perm action quotient gproduct cyclic center) mathcomp(pgroup nilpotent sylow hall abelian)