proposition: Lemma p_index_maximal : M \subset P -> prime #|P : M| -> maximal M P.
proof: Proof. move=> sMP /primeP[lt1PM pr_PM]. apply/maxgroupP; rewrite properEcard sMP -(Lagrange sMP). rewrite -{1}(muln1 #|M|) ltn_pmul2l //; split=> // H sHP sMH. apply/eqP; rewrite eq_sym eqEcard sMH. case/orP: (pr_PM _ (indexSg sMH (proper_sub sHP))) => /eqP iM. by rewrite -(Lagrange sMH) iM muln1 /=. by have:= proper_card sHP; rewrite -(Lagrange sMH) iM Lagrange ?ltnn. 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)