proposition: Lemma pHallP pi G H : reflect (H \subset G /\ #|H| = #|G|`_pi) (pi.-Hall(G) H).
proof: Proof. apply: (iffP idP) => [piH | [sHG oH]]. by split; [apply: pHall_sub piH | apply: card_Hall]. rewrite /pHall sHG -divgS // /pgroup oH. by rewrite -{2}(@partnC pi #|G|) ?mulKn ?part_pnat. 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)