proposition: Lemma setI_normal_Hall G H K : H <| G -> pi.-Hall(G) H -> K \subset G -> pi.-Hall(K) (H :&: K).
proof: Proof. move=> nsHG hallH sKG; apply: normal_max_pgroup_Hall; last first. by rewrite /= setIC (normalGI sKG nsHG). apply/maxgroupP; split=> [|M /andP[sMK piM] sHK_M]. by rewrite /psubgroup subsetIr (pgroupS (subsetIl _ _) (pHall_pgroup hallH)). apply/eqP; rewrite eqEsubset sHK_M subsetI sMK !andbT. by rewrite (sub_normal_Hall hallH) // (subset_trans sMK). 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)