proposition: Lemma Puig_limit G : exists m, forall k, m <= k -> 'L_{k.*2}(G) = 'L_*(G) /\ 'L_{k.*2.+1}(G) = 'L(G).
proof: Proof. pose L2G m := 'L_{m.*2}(G); pose n := #|G|. have []: #|L2G n| <= n /\ n <= n by rewrite subset_leq_card ?Puig_at_sub. elim: {1 2 3}n => [| m IHm leLm1 /ltnW]; first by rewrite leqNgt cardG_gt0. have [eqLm le_mn|] := eqVneq (L2G m.+1) (L2G m); last first. rewrite eq_sym eqEcard Puig_sub_even ?leqnSn // -ltnNge => lt_m1_m. exact: IHm (leq_trans lt_m1_m leLm1). have{} eqLm k: m <= k -> 'L_{k.*2}(G) = L2G m. rewrite leq_eqVlt => /predU1P[-> // |]; elim: k => // k IHk. by rewrite leq_eqVlt => /predU1P[<- //| ltmk]; rewrite -eqLm !PuigS IHk. by exists m => k le_mk; rewrite Puig_def PuigS /Puig_inf /= !eqLm. 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)