proposition: Proposition sigma'_not_uniq K : K \subset M -> sigma'.-group K -> K \notin 'U.
proof: Proof. move=> sKM sg'K; have [E hallE sKE] := Hall_superset solM sKM sg'K. have [sEM sg'E _] := and3P hallE. have rEle2: 'r(E) <= 2. have [q _ ->] := rank_witness E; rewrite leqNgt; apply/negP=> rEgt2. have: q \in sigma' by rewrite (pnatPpi sg'E) // -p_rank_gt0 -(subnKC rEgt2). by rewrite inE /= alpha_sub_sigma //; apply: leq_trans (p_rankS q sEM). have [E1 | ntE]:= eqsVneq E 1. by apply: contraL (@uniq_mmax_neq1 _ K) _; rewrite -subG1 -E1. pose p := max_pdiv #|E|; pose P := 'O_p(E). have piEp: p \in \pi(E) by rewrite pi_max_pdiv cardG_gt1. have sg'p: p \in sigma' by rewrite (pnatPpi sg'E). have sylP: p.-Sylow(E) P. rewrite rank2_max_pcore_Sylow ?mFT_odd ?(solvableS sEM solM) //. exact: leq_trans (rankS (Fitting_sub E)) rEle2. apply: contra (sg'p) => uniqK; apply/existsP; exists [group of P]. have defMK := def_uniq_mmax uniqK maxM (subset_trans sKE sEM). rewrite (subHall_Sylow hallE) // (sub_uniq_mmax defMK) //; last first. rewrite mFT_norm_proper ?(mFT_pgroup_proper (pcore_pgroup _ _)) //. by rewrite -cardG_gt1 (card_Hall sylP) p_part_gt1. by rewrite (subset_trans sKE) // gFnorm. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype) mathcomp(bigop finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9)