proposition: Lemma Hall_setI_normal pi G K H : K <| G -> pi.-Hall(G) H -> pi.-Hall(K) (H :&: K).
proof: Proof. move=> nsKG hallH; have [sHG piH _] := and3P hallH. have [sHK_H sHK_K] := (subsetIl H K, subsetIr H K). rewrite pHallE sHK_K /= -(part_pnat_id (pgroupS sHK_H piH)); apply/eqP. rewrite (widen_partn _ (subset_leq_card sHK_K)); apply: eq_bigr => p pi_p. have [P sylP] := Sylow_exists p H. have sylPK := Sylow_setI_normal nsKG (subHall_Sylow hallH pi_p sylP). rewrite -!p_part -(card_Hall sylPK); symmetry; apply: card_Hall. by rewrite (pHall_subl _ sHK_K) //= setIC setSI ?(pHall_sub sylP). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype prime bigop finset fingroup morphism) mathcomp(automorphism quotient action cyclic gproduct) mathcomp(gfunctor commutator pgroup center nilpotent)