proposition: Theorem rank2_der1_sub_Fitting gT (G : {group gT}) : odd #|G| -> solvable G -> 'r('F(G)) <= 2 -> G^`(1) \subset 'F(G).
proof: Proof. move=> oddG solG Fle2; have nsFG := Fitting_normal G. apply: subset_trans (chief_stab_sub_Fitting solG _) => //. rewrite subsetI der_sub; apply/bigcapsP=> [[U V] /= /andP[chiefUV sUF]]. have [p p_pr /andP[pUV _]] := is_abelemP (sol_chief_abelem solG chiefUV). apply: rank2_der1_cent_chief nsFG _ _ pUV sUF => //. exact: leq_trans (p_rank_le_rank p _) Fle2. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype finfun bigop ssralg finset prime binomial) mathcomp(fingroup morphism automorphism perm quotient action gproduct) mathcomp(gfunctor commutator zmodp cyclic center pgroup gseries nilpotent) mathcomp(sylow abelian maximal extremal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1 BGsection2)