proposition: Lemma nonTI_Fitting_facts M : M \in 'M -> ~~ normedTI 'F(M)^# G M -> [/\ M \in 'M_'F :|: 'M_'P1, M`_\F = M`_\sigma & M^`(1) \subset 'F(M)].
proof: Proof. move=> maxM nonTI; suff: [exists (y | y \notin M), 'F(M) :&: 'F(M) :^ y != 1]. by case/exists_inP=> y notMy /nonTI_Fitting_structure[] // [-> dMF] _ []. rewrite -negb_forall_in; apply: contra nonTI => /forall_inP tiF. apply/normedTI_P; rewrite normD1 setTI gFnorm setD_eq0 subG1. split=> // [|g _]; first by rewrite (trivg_Fitting (mmax_sol maxM)) mmax_neq1. by apply: contraR => /tiF; rewrite -setI_eq0 conjD1g -setDIl setD_eq0 subG1. 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 BGsection2 BGsection3 BGsection4 BGsection5) odd_order(BGsection6 BGsection7 BGsection9 BGsection10 BGsection12) odd_order(BGsection13 BGsection14)