proposition: Lemma nil_class_pgroup (gT : finGroupType) (p : nat) (P : {group gT}) : p.-group P -> nil_class P <= maxn 1 (logn p #|P|).-1.
proof: Proof. move=> pP; move def_c: (nil_class P) => c. elim: c => // c IHc in gT P def_c pP *; set e := logn p _. have nilP := pgroup_nil pP; have sZP := center_sub P. have [e_le2 | e_gt2] := leqP e 2. by rewrite -def_c leq_max nil_class1 (p2group_abelian pP). have pPq: p.-group (P / 'Z(P)) by apply: quotient_pgroup. rewrite -(subnKC e_gt2) ltnS (leq_trans (IHc _ _ _ pPq)) //. by rewrite nil_class_quotient_center ?def_c. rewrite geq_max /= -add1n -leq_subLR -subn1 -subnDA -subSS leq_sub2r //. rewrite ltn_log_quotient //= -(setIidPr sZP) meet_center_nil //. by rewrite -nil_class0 def_c. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype prime bigop finset fingroup morphism) mathcomp(automorphism quotient action cyclic gproduct) mathcomp(gfunctor commutator pgroup center nilpotent)