proposition: Lemma sub_normal_Hall pi G H K : pi.-Hall(G) H -> H <| G -> K \subset G -> (K \subset H) = pi.-group K.
proof: Proof. move=> hallH nsHG sKG; apply/idP/idP=> [sKH | piK]. by rewrite (pgroupS sKH) ?(pHall_pgroup hallH). apply: norm_sub_max_pgroup (Hall_max hallH) piK _ _ => //. exact: subset_trans sKG (normal_norm nsHG). 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)