proposition: Lemma Frobenius_partition : partition (gval K |: (H^# :^: K)) G.
proof: Proof. have [/eqP defG _ tiHG] := and3P frobG; have [_ tiH1G /eqP defN] := and3P tiHG. have [[_ /mulG_sub[sKG sHG] nKH tiKH] mulHK] := (sdprodP defG, sdprodWC defG). set HG := H^# :^: K; set KHG := _ |: _. have defHG: HG = H^# :^: G. have: 'C_G[H^# | 'Js] * K = G by rewrite astab1Js defN mulHK. move/subgroup_transitiveP/atransP. by apply; rewrite ?atrans_orbit ?orbit_refl. have /and3P[defHK _ nzHG] := partition_normedTI tiHG. rewrite -defHG in defHK nzHG tiH1G. have [tiKHG HG'K]: trivIset KHG /\ gval K \notin HG. apply: trivIsetU1 => // _ /imsetP[x Kx ->]; rewrite -setI_eq0. by rewrite -(conjGid Kx) -conjIg setIDA tiKH setDv conj0g. rewrite /partition andbC tiKHG !inE negb_or nzHG eq_sym -card_gt0 cardG_gt0 /=. rewrite eqEcard; apply/andP; split. rewrite /cover big_setU1 //= subUset sKG -/(cover HG) (eqP defHK). by rewrite class_support_subG // (subset_trans _ sHG) ?subD1set. rewrite -(eqnP tiKHG) big_setU1 //= (eqnP tiH1G) (eqP defHK). rewrite (card_support_normedTI tiHG) -(Lagrange sHG) (cardsD1 1) group1 mulSn. by rewrite leq_add2r -mulHK indexMg -indexgI tiKH indexg1. 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)