proposition: Lemma pcore_Sylow_Puig_sub : 'L_*(S) \subset 'L_*(T) /\ 'L(T) \subset 'L(S).
proof: Proof. have [[kS defLS] [kT defLT]] := (Puig_limit S, Puig_limit [group of T]). have [/defLS[<- <-] /defLT[<- <-]] := (leq_maxl kS kT, leq_maxr kS kT). have sL_ := subset_trans (Puig_succ_sub _ _). elim: (maxn kS kT) => [|k [_ sL1]]; first by rewrite !Puig1 pcore_sub_Hall. have{sL1} gL: 'L_{k.*2.+1}(T) --> 'L_{k.*2.+2}(S). exact: norm_abgenS sL1 (Puig_gen _ _). have sCT_L: 'C_T('L_{k.*2.+1}(T)) \subset 'L_{k.*2.+1}(T). exact: sub_cent_Puig_at pT. have{sCT_L} sLT: 'L_{k.*2.+2}(S) \subset T. apply: odd_abelian_gen_constrained sCT_L => //. - exact: pgroupS (Puig_at_sub _ _) pT. - exact: gFnormal_trans nsTG. - exact: sL_ sSG. by rewrite norm_abgen_pgroup // (pgroupS _ pS) ?Puig_at_sub. have sL2: 'L_{k.*2.+2}(S) \subset 'L_{k.*2.+2}(T) by apply: Puig_max. split; [exact: sL2 | rewrite doubleS; apply: subset_trans (Puig_succS _ sL2) _]. by rewrite Puig_max -?PuigS ?Puig_gen // sL_ // pcore_sub_Hall. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop prime finset ssralg fingroup morphism) mathcomp(automorphism quotient gfunctor commutator zmodp center pgroup) mathcomp(sylow gseries nilpotent abelian maximal) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1 BGsection2)