proposition: Lemma lcn_nil_classP n G : nilpotent G -> reflect ('L_n.+1(G) = 1) (nil_class G <= n).
proof: Proof. rewrite nilpotent_class /nil_class; set s := mkseq _ _. set c := index 1 s => lt_c_G; case: leqP => [le_c_n | lt_n_c]. have Lc1: nth 1 s c = 1 by rewrite nth_index // -index_mem size_mkseq. by left; apply/trivgP; rewrite -Lc1 nth_mkseq ?lcn_sub_leq. right; apply/eqP/negPf; rewrite -(before_find 1 lt_n_c) nth_mkseq //. exact: ltn_trans lt_n_c lt_c_G. 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)