proposition: Lemma Thompson_critical : p.-group G -> {K : {group gT} | critical K G}.
proof: Proof. move=> pG; pose qcr A := (A \char G) && ('Phi(A) :|: [~: G, A] \subset 'Z(A)). have [|K]:= @maxgroup_exists _ qcr 1 _. by rewrite /qcr char1 center1 commG1 subUset Phi_sub subxx. case/maxgroupP; rewrite {}/qcr subUset => /and3P[chK sPhiZ sRZ] maxK _. have sKG := char_sub chK; have nKG := char_normal chK. exists K; split=> //; apply/eqP; rewrite eqEsubset andbC setSI //=. have chZ: 'Z(K) \char G by [apply: subcent_char]; have nZG := char_norm chZ. have chC: 'C_G(K) \char G by apply: subcent_char chK. rewrite -quotient_sub1; last by rewrite subIset // char_norm. apply/trivgP; apply: (TI_center_nil (quotient_nil _ (pgroup_nil pG))). by rewrite quotient_normal ?norm_normalI ?norms_cent ?normal_norm. apply: TI_Ohm1; apply/trivgP; rewrite -trivg_quotient -sub_cosetpre_quo //. rewrite morphpreI quotientGK /=; last first. by apply: normalS (char_normal chZ); rewrite ?subsetIl ?setSI. set X := _ :&: _; pose gX := [group of X]. have sXG: X \subset G by rewrite subIset ?subsetIl. have cXK: K \subset 'C(gX) by rewrite centsC 2?subIset // subxx orbT. rewrite subsetI centsC cXK andbT -(mul1g K) -mulSG mul1g -(cent_joinEr cXK). rewrite [_ <*> K]maxK ?joing_subr //= andbC (cent_joinEr cXK). rewrite -center_prod // (subset_trans _ (mulG_subr _ _)). rewrite charM 1?charI ?(char_from_quotient (normal_cosetpre _)) //. by rewrite cosetpreK !gFchar_trans. rewrite (@Phi_mulg p) ?(pgroupS _ pG) // subUset commGC commMG; last first. by rewrite normsR ?(normsG sKG) // cents_norm // centsC. rewrite !mul_subG 1?commGC //. apply: subset_trans (commgS _ (subsetIr _ _)) _. rewrite -quotient_cents2 ?subsetIl // centsC // cosetpreK //. exact/gFsub_trans/subsetIr. have nZX := subset_trans sXG nZG; have pX : p.-group gX by apply: pgroupS pG. rewrite -quotient_sub1 ?gFsub_trans //=. have pXZ: p.-group (gX / 'Z(K)) by apply: morphim_pgroup. rewrite (quotient_Phi pX nZX) subG1 (trivg_Phi pXZ). apply: (abelemS (quotientS _ (subsetIr _ _))); rewrite /= cosetpreK /=. have pZ: p.-group 'Z(G / 'Z(K)). by rewrite (pgroupS (center_sub _)) ?morphim_pgroup. by rewrite Ohm1_abelem ?center_abelian. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism quotient) mathcomp(action commutator gproduct gfunctor ssralg) mathcomp(countalg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule)