proposition: Lemma exponent_witness G : nilpotent G -> {x | x \in G & exponent G = #[x]}.
proof: Proof. move=> nilG; have [//=| /= x Gx max_x] := @arg_maxnP _ 1 [in G] order. exists x => //; apply/eqP; rewrite eqn_dvd dvdn_exponent // andbT. apply/dvdn_biglcmP=> y Gy; apply/dvdn_partP=> //= p. rewrite mem_primes => /andP[p_pr _]; have p_gt1: p > 1 := prime_gt1 p_pr. rewrite p_part pfactor_dvdn // -(leq_exp2l _ _ p_gt1) -!p_part. rewrite -(leq_pmul2r (part_gt0 p^' #[x])) partnC // -!order_constt. rewrite -orderM ?order_constt ?coprime_partC // ?max_x ?groupM ?groupX //. case/dprodP: (nilpotent_pcoreC p nilG) => _ _ cGpGp' _. have inGp := mem_normal_Hall (nilpotent_pcore_Hall _ nilG) (pcore_normal _ _). by red; rewrite -(centsP cGpGp') // inGp ?p_elt_constt ?groupX. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism action) mathcomp(quotient gfunctor gproduct ssralg countalg finalg zmodp) mathcomp(cyclic pgroup gseries nilpotent sylow)