proposition: Lemma pHall_Hall pi A B : pi.-Hall(A) B -> Hall A B.
proof: Proof. by case/and3P=> sBA piB pi'B; rewrite /Hall sBA (pnat_coprime piB). 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)