proposition: Remark tau3E p : (p \in \tau3(M)) = (p \in \pi(E^`(1))) && ('r_p(E) == 1%N).
proof: Proof. have [P sylP] := Sylow_exists p E. have hallE': \sigma(M)^'.-Hall(M^`(1)) E^`(1). by rewrite -der1_sigma_compl setIC (Hall_setI_normal _ hallE) ?der_normal. rewrite 4!inE -(andb_idl (pnatPpi (pHall_pgroup hallE'))) -andbA. apply: andb_id2l => s'p; have sylP_M := subHall_Sylow hallE s'p sylP. rewrite -(p_rank_Sylow sylP_M) (p_rank_Sylow sylP) andbC; apply: andb_id2r. rewrite eqn_leq p_rank_gt0 mem_primes => /and3P[_ p_pr _]. rewrite (card_Hall hallE') pi_of_part 3?inE ?mem_primes ?cardG_gt0 //=. by rewrite p_pr inE /= s'p andbT. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq choice div fintype) mathcomp(path bigop finset prime fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor pgroup cyclic commutator) mathcomp(center gseries nilpotent sylow abelian maximal hall frobenius) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection11)