proposition: Lemma p_maximal_index : maximal M P -> #|P : M| = p.
proof: Proof. move=> maxM; have nM := p_maximal_normal maxM. rewrite -card_quotient ?normal_norm //. rewrite -(quotient_maximal _ nM) ?normal_refl // trivg_quotient in maxM. case/maxgroupP: maxM; rewrite properEneq eq_sym sub1G andbT /=. case/(pgroup_pdiv (quotient_pgroup M pP)) => p_pr /Cauchy[] // xq. rewrite /order -cycle_subG subEproper => /predU1P[-> // | sxPq oxq_p _]. by move/(_ _ sxPq (sub1G _)) => xq1; rewrite -oxq_p xq1 cards1 in p_pr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism quotient) mathcomp(action commutator gproduct gfunctor ssralg) mathcomp(countalg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule)