proposition: Lemma Frobenius_kerP G K : reflect [/\ K :!=: 1, K \proper G, K <| G & {in K^#, forall x, 'C_G[x] \subset K}] [Frobenius G with kernel K].
proof: Proof. apply: (iffP existsP) => [[H frobG] | [ntK ltKG nsKG regK]]. have [/sdprod_context[nsKG _ _ _ _] ntK _ ltKG _] := Frobenius_context frobG. by split=> //; apply: Frobenius_cent1_ker frobG. have /andP[sKG nKG] := nsKG. have hallK: Hall G K. rewrite /Hall sKG //= coprime_sym coprime_pi' //. apply: sub_pgroup (pgroup_pi K) => p; have [P sylP] := Sylow_exists p G. have [[sPG pP p'GiP] sylPK] := (and3P sylP, Hall_setI_normal nsKG sylP). rewrite -p_rank_gt0 -(rank_Sylow sylPK) rank_gt0 => ntPK. rewrite inE /= -p'natEpi // (pnat_dvd _ p'GiP) ?indexgS //. have /trivgPn[z]: P :&: K :&: 'Z(P) != 1. by rewrite meet_center_nil ?(pgroup_nil pP) ?(normalGI sPG nsKG). rewrite !inE -andbA -sub_cent1=> /and4P[_ Kz _ cPz] ntz. by apply: subset_trans (regK z _); [apply/subsetIP | apply/setD1P]. have /splitsP[H /complP[tiKH defG]] := SchurZassenhaus_split hallK nsKG. have [_ sHG] := mulG_sub defG; have nKH := subset_trans sHG nKG. exists H; apply/Frobenius_semiregularP; rewrite ?sdprodE //. by apply: contraNneq (proper_subn ltKG) => H1; rewrite -defG H1 mulg1. apply: semiregular_sym => x Kx; apply/trivgP; rewrite -tiKH. by rewrite subsetI subsetIl (subset_trans _ (regK x _)) ?setSI. 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)