proposition: Lemma sub_pHall pi H G K : pi.-Hall(G) H -> pi.-group K -> H \subset K -> K \subset G -> K :=: H.
proof: Proof. move=> hallH piK sHK sKG; apply/eqP; rewrite eq_sym eqEcard sHK. by rewrite (card_Hall hallH) -(part_pnat_id piK) dvdn_leq ?partn_dvd ?cardSg. 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)