proposition: Remark tau1E p : (p \in \tau1(M)) = [&& p \in \pi(E), p \notin \pi(E^`(1)) & 'r_p(E) == 1%N].
proof: Proof. rewrite partition_pi_sigma_compl; apply/idP/idP=> [t1p|]. have [s'p rpM _] := and3P t1p; have [P sylP] := Sylow_exists p E. have:= tau3'1 t1p; rewrite t1p /= inE /= tau3E -(p_rank_Sylow sylP). by rewrite (p_rank_Sylow (subHall_Sylow hallE s'p sylP)) rpM !andbT. rewrite orbC andbC -andbA => /and3P[not_piE'p /eqP rpE]. by rewrite tau3E tau2E rpE (negPf not_piE'p) andbF. 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)