proposition: Lemma pmorphim_pHall pi G H : G \subset D -> H \subset D -> pi.-subgroup(H :&: G) ('ker f) -> pi.-Hall(f @* G) (f @* H) = pi.-Hall(G) H.
proof: Proof. move=> sGD sHD /andP[/subsetIP[sKH sKG] piK]; rewrite !pHallE morphimSGK //. apply: andb_id2l => sHG; rewrite -(Lagrange sKH) -(Lagrange sKG) partnM //. by rewrite (part_pnat_id piK) !card_morphim !(setIidPr _) // eqn_pmul2l. 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)