proposition: Lemma der1_quo_sigma' : p %| #|M / M^`(1)| -> p \in \sigma(M)^'.
proof: Proof. apply: contraL => /= s_p; have piMp := sigma_sub_pi maxM s_p. have p_pr: prime p by move: piMp; rewrite mem_primes; case/andP. rewrite -p'natE ?(pi'_p'nat _ s_p) // -pgroupE -partG_eq1. rewrite -(card_Hall (quotient_pHall _ Msigma_Hall)) /=; last first. exact/gFsub_trans/gFnorm. by rewrite quotientS1 ?cards1 // Msigma_der1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype) mathcomp(bigop finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9)