proposition: Lemma rank_witness G : {p | prime p & 'r(G) = 'r_p(G)}.
proof: Proof. have [p _ defmG]: {p : 'I_(#|G|.+1) | true & 'r(G) = 'r_p(G)}. by rewrite ['r(G)]big_mkord; apply: eq_bigmax_cond; rewrite card_ord. case: (eqsVneq G 1) => [-> | ]; first by exists 2; rewrite // rank1 p_rank1. by rewrite -rank_gt0 defmG p_rank_gt0 mem_primes; case/andP; exists p. 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)