proposition: Lemma ell_sigma0P x : reflect (x = 1) (\ell_\sigma(x) == 0).
proof: Proof. rewrite cards_eq0 setD_eq0. apply: (iffP idP) => [x1 | ->]; last first. by apply/subsetP=> _ /imsetP[M _ ->]; rewrite constt1 inE. rewrite -(prod_constt x) big1_seq //= => p _; apply: contraTeq x1 => nt_xp. have piXp: p \in \pi(#[x]) by rewrite -p_part_gt1 -order_constt order_gt1. have [M maxM sMp] := sigma_mmax_exists (piSg (subsetT _) piXp). apply/subsetPn; exists (x.`_(\sigma(M))); first exact: imset_f. by rewrite (sameP set1P constt1P); apply: contraL sMp => /pnatPpi; apply. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype bigop order) mathcomp(finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall frobenius) mathcomp(ssralg ssrnum ssrint rat) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection12 BGsection13)