proposition: Lemma sub_Puig_eq G H : H \subset G -> 'L(G) \subset H -> 'L(H) = 'L(G).
proof: Proof. move=> sHG sLG_H; apply/setP/subset_eqP/andP. have sLH_G := subset_trans (Puig_succ_sub _ _) sHG. have gPuig := norm_abgenS _ (Puig_gen _ _). have [[kG defLG] [kH defLH]] := (Puig_limit G, Puig_limit H). have [/defLG[_ {1}<-] /defLH[_ <-]] := (leq_maxl kG kH, leq_maxr kG kH). split; do [elim: (maxn _ _) => [|k IHk /=]; first by rewrite !Puig1]. rewrite doubleS !(PuigS _.+1) Puig_max ?gPuig // Puig_max ?gPuig //. exact: subset_trans (Puig_sub_even_odd _.+1 _ _) sLG_H. rewrite doubleS Puig_max // -!PuigS Puig_def gPuig //. by rewrite Puig_inf_def Puig_max ?gPuig ?sLH_G. 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)