proposition: Lemma subHall_Hall pi rho G H K : rho.-Hall(G) H -> {subset pi <= rho} -> pi.-Hall(H) K -> pi.-Hall(G) K.
proof: Proof. move=> hallH pi_sub_rho hallK. rewrite pHallE (subset_trans (pHall_sub hallK) (pHall_sub hallH)) /=. by rewrite (card_Hall hallK) (card_Hall hallH) partn_part. 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)