proposition: Lemma ex_kappa_compl M K : M \in 'M -> \kappa(M).-Hall(M) K -> exists U : {group gT}, kappa_complement M U K.
proof: Proof. move=> maxM hallK; have [sKM kK _] := and3P hallK. have s'K: \sigma(M)^'.-group K := sub_pgroup (@kappa_sigma' M) kK. have [E hallE sKE] := Hall_superset (mmax_sol maxM) sKM s'K. pose sk' := \sigma_kappa(M)^'. have [U hallU] := Hall_exists sk' (sigma_compl_sol hallE). exists U; split=> //. by apply: subHall_Hall hallE _ hallU => p; case/norP. suffices ->: U * K = E by apply: groupP. have [[sUE sk'U _] [sEM s'E _]] := (and3P hallU, and3P hallE). apply/eqP; rewrite eqEcard mulG_subG sUE sKE /= coprime_cardMg; last first. by apply: p'nat_coprime (sub_pgroup _ sk'U) kK => p; case/norP. rewrite -(partnC \kappa(M) (cardG_gt0 E)) -{2}(part_pnat_id s'E) mulnC. rewrite -(card_Hall (pHall_subl sKE sEM hallK)) leq_mul // -partnI. by rewrite -(@eq_partn sk') -?(card_Hall hallU) // => p; apply: negb_or. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype bigop order) mathcomp(finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall frobenius) mathcomp(ssralg ssrnum ssrint rat) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection12 BGsection13)