proposition: Lemma lcnP G : reflect (exists n, 'L_n.+1(G) = 1) (nilpotent G).
proof: Proof. apply: (iffP idP) => [nilG | [n Ln1]]. by exists (nil_class G); apply/lcn_nil_classP. apply/forall_inP=> H /subsetIP[sHG sHR]; rewrite -subG1 -{}Ln1. by elim: n => // n IHn; rewrite (subset_trans sHR) ?commSg. 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)