proposition: Lemma subHall_Sylow pi p G H P : pi.-Hall(G) H -> p \in pi -> p.-Sylow(H) P -> p.-Sylow(G) P.
proof: Proof. move=> hallH pi_p sylP; have [sHG piH _] := and3P hallH. rewrite pHallE (subset_trans (pHall_sub sylP) sHG) /=. by rewrite (card_Hall sylP) (card_Hall hallH) partn_part // => q; move/eqnP->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup morphism) mathcomp(gfunctor automorphism quotient action gproduct) mathcomp(cyclic)