proposition: Theorem mFT_proper_plength1 p H : H \proper G -> p.-length_1 H.
proof: Proof. case/mmax_exists=> M /setIdP[maxM sHM]. suffices{H sHM}: p.-length_1 M by apply: plength1S. have [solM oddM] := (mmax_sol maxM, mFT_odd M). have [rpMle2 | a_p] := leqP 'r_p(M) 2. by rewrite plength1_pseries2_quo; case/rank2_der1_complement: rpMle2. pose Ma := M`_\alpha; have hallMa: \alpha(M).-Hall(M) Ma := Malpha_Hall maxM. have [[K hallK] [sMaM aMa _]] := (Hall_exists \alpha(M)^' solM, and3P hallMa). have defM: Ma ><| K = M by apply/sdprod_Hall_pcoreP. have{aMa} coMaK: coprime #|Ma| #|K| := pnat_coprime aMa (pHall_pgroup hallK). suffices{a_p hallMa}: p.-length_1 Ma. rewrite !p_elt_gen_length1 /p_elt_gen setIdE /= -/Ma -(setIidPl sMaM) -setIA. rewrite -(setIdE M) (setIidPr _) //; apply/subsetP=> x; case/setIdP=> Mx p_x. by rewrite (mem_Hall_pcore hallMa) /p_elt ?(pi_pnat p_x). have{sMaM} <-: [~: Ma, K] = Ma. have sMaMs: Ma \subset M`_\sigma := Malpha_sub_Msigma maxM. have sMaM': Ma \subset M^`(1) := subset_trans sMaMs (Msigma_der1 maxM). by have [] := coprime_der1_sdprod defM coMaK (solvableS sMaM solM) sMaM'. have [q q_pr q_dv_Mq]: {q | prime q & q %| #|M / M^`(1)| }. apply: pdivP; rewrite card_quotient ?der_norm // indexg_gt1 proper_subn //. by rewrite (sol_der1_proper solM) ?mmax_neq1. have s'q: q \in \sigma(M)^' by apply: der1_quo_sigma' q_dv_Mq. have [Q sylQ] := Sylow_exists q K; have [sQK qQ _] := and3P sylQ. have a'q: q \in \alpha(M)^' by apply: contra s'q; apply: alpha_sub_sigma. have{a'q hallK} sylQ: q.-Sylow(M) Q := subHall_Sylow hallK a'q sylQ. have{q_dv_Mq} ntQ: Q :!=: 1. rewrite -rank_gt0 (rank_Sylow sylQ) p_rank_gt0 mem_primes q_pr cardG_gt0. exact: dvdn_trans q_dv_Mq (dvdn_quotient _ _). have{s'q sylQ ntQ} [x [Q1x _ ZgCx]] := cent1_sigma'_Zgroup maxM s'q sylQ ntQ. have{Q1x} [ntx Q1x] := setD1P Q1x. have sZQ := center_sub Q; have{sQK} sZK := subset_trans sZQ sQK. have{sZK} Kx: x \in K by rewrite (subsetP sZK) // (subsetP (Ohm_sub 1 _)). have{sZQ qQ} abelQ1 := Ohm1_abelem (pgroupS sZQ qQ) (center_abelian Q). have{q q_pr Q abelQ1 Q1x} ox: prime #[x] by rewrite (abelem_order_p abelQ1). move: Kx ox ZgCx; rewrite -cycle_subG -cent_cycle. exact: odd_sdprod_Zgroup_cent_prime_plength1 solM oddM defM coMaK. 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)