proposition: Corollary tau2_compl_abelian M E E2 : M \in 'M -> \sigma(M)^'.-Hall(M) E -> \tau2(M).-Hall(E) E2 -> abelian E2.
proof: Proof. move: E2 => F2 maxM hallE hallF2; have [sEM s'E _] := and3P hallE. have [[E1 hallE1] [E3 hallE3]] := ex_tau13_compl hallE. have [E2 hallE2 complEi] := ex_tau2_compl hallE hallE1 hallE3. have solE: solvable E := sigma_compl_sol hallE. have{solE hallF2} [x _ ->{F2}] := Hall_trans solE hallF2 hallE2. have [-> | ntE] := eqsVneq E2 1; rewrite {x}abelianJ ?abelian1 //. have [[p p_pr rpE2] [sE2E t2E2 _]] := (rank_witness E2, and3P hallE2). have piE2p: p \in \pi(E2) by rewrite -p_rank_gt0 -rpE2 rank_gt0. have t2p := pnatPpi t2E2 piE2p; have [A Ep2A _] := ex_tau2Elem hallE t2p. have [_ abelA _] := pnElemP Ep2A; have [pA _] := andP abelA. have [S /= sylS sAS] := Sylow_superset (subsetT A) pA. have [cSS | not_cSS] := boolP (abelian S). by have [[_ cE2E2] _ _ _] := abelian_tau2 maxM complEi t2p Ep2A sylS sAS cSS. have pS := pHall_pgroup sylS. have [def_t2 _ _ _] := nonabelian_tau2 maxM hallE t2p Ep2A pS not_cSS. apply: sigma'_nil_abelian (subset_trans _ sEM) (pgroupS _ s'E) _ => //. by rewrite (eq_pgroup _ def_t2) in t2E2; apply: pgroup_nil t2E2. 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)