proposition: Lemma nilpotent_class G : nilpotent G = (nil_class G < #|G|).
proof: Proof. rewrite /nil_class; set s := mkseq _ _. transitivity (1 \in s); last by rewrite -index_mem size_mkseq. apply/idP/mapP=> {s}/= [nilG | [n _ Ln1]]; last first. apply/forall_inP=> H /subsetIP[sHG sHR]. rewrite -subG1 {}Ln1; elim: n => // n IHn. by rewrite (subset_trans sHR) ?commSg. pose m := #|G|.-1; exists m; first by rewrite mem_iota /= prednK. set n := m; rewrite ['L__(G)]card_le1_trivg //= -(subnn m) -[m in _ - m]/n. elim: n => [|n]; [by rewrite subn0 prednK | rewrite lcnSn subnS]. case: (eqsVneq 'L_n.+1(G) 1) => [-> | ntLn]; first by rewrite comm1G cards1. case: (m - n) => [|m' /= IHn]; first by rewrite leqNgt cardG_gt1 ntLn. rewrite -ltnS (leq_trans (proper_card _) IHn) //. by rewrite (nil_comm_properl nilG) ?lcn_sub // subsetI subxx lcn_norm. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype div bigop prime finset fingroup morphism) mathcomp(automorphism quotient commutator gproduct) mathcomp(gfunctor center gseries cyclic)