proposition: Lemma ex_tau2_compl E1 E3 : \tau1(M).-Hall(E) E1 -> \tau3(M).-Hall(E) E3 -> exists2 E2 : {group gT}, \tau2(M).-Hall(E) E2 & sigma_complement M E E1 E2 E3.
proof: Proof. move=> hallE1 hallE3; have [sE1E t1E1 _] := and3P hallE1. pose tau12 := [predU \tau1(M) & \tau2(M)]. have t12E1: tau12.-group E1 by apply: sub_pgroup t1E1 => p t1p; apply/orP; left. have [E21 hallE21 sE1E21] := Hall_superset solE sE1E t12E1. have [sE21E t12E21 _] := and3P hallE21. have [E2 hallE2] := Hall_exists \tau2(M) (solvableS sE21E solE). have [sE2E21 t2E2 _] := and3P hallE2. have hallE2_E: \tau2(M).-Hall(E) E2. by apply: subHall_Hall hallE21 _ hallE2 => p t2p; apply/orP; right. exists E2 => //; split=> //. suffices ->: E2 * E1 = E21 by apply: groupP. have coE21: coprime #|E2| #|E1| := sub_pnat_coprime tau2'1 t2E2 t1E1. apply/eqP; rewrite eqEcard mul_subG ?coprime_cardMg //=. rewrite -(partnC \tau1(M) (cardG_gt0 E21)) (card_Hall hallE2) mulnC. rewrite (card_Hall (pHall_subl sE1E21 sE21E hallE1)) leq_pmul2r //. rewrite dvdn_leq // sub_in_partn // => p t12p t1'p. by apply: contraLR (pnatPpi t12E21 t12p) => t2'p; apply/norP. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq choice div fintype) mathcomp(path bigop finset prime fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor pgroup cyclic commutator) mathcomp(center gseries nilpotent sylow abelian maximal hall frobenius) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection11)