proposition: Proposition plength_1_normed_constrained p A : A :!=: 1 -> A \in 'E*_p(G) -> (forall M, M \proper G -> p.-length_1 M) -> normed_constrained A.
proof: Proof. move=> ntA EpA pl1subG. case/pmaxElemP: (EpA); case/pElemP=> sAG; case/and3P=> pA cAA _ _. have prA: A \proper G := sub_proper_trans cAA (mFT_cent_proper ntA). split=> // X Y sAX prX; case/setIdP; case/andP=> sYX p'Y nYA. have pl1X := pl1subG _ prX; have solX := mFT_sol prX. have [p_pr _ [r oApr]] := pgroup_pdiv pA ntA. have oddp: odd p by move: (mFT_odd A); rewrite oApr oddX. have def_pi: \pi(A)^' =i p^'. by move=> q; rewrite inE /= oApr pi_of_exp // pi_of_prime. have{} p'Y : p^'.-group Y by rewrite -(eq_pgroup _ def_pi). rewrite (eq_pcore _ def_pi) (@plength1_norm_pmaxElem _ p X A) //. by rewrite (subsetP (pmaxElemS p (subsetT _))) // setIC 2!inE sAX. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div choice fintype bigop) mathcomp(finset prime fingroup morphism automorphism action quotient) mathcomp(gfunctor cyclic pgroup center commutator gseries nilpotent) mathcomp(sylow abelian maximal hall) odd_order(BGsection1 BGsection6)