proposition: Lemma pgroup_nil p P : p.-group P -> nilpotent P.
proof: Proof. move: {2}_.+1 (ltnSn #|P|) => n. elim: n gT P => // n IHn pT P; rewrite ltnS=> lePn pP. have [Z1 | ntZ] := eqVneq 'Z(P) 1. by rewrite (trivg_center_pgroup pP Z1) nilpotent1. rewrite -quotient_center_nil IHn ?morphim_pgroup // (leq_trans _ lePn) //. rewrite card_quotient ?normal_norm ?center_normal // -divgS ?subsetIl //. by rewrite ltn_Pdiv // ltnNge -trivg_card_le1. 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)