proposition: Lemma morphim_pHall pi G H : H \subset D -> pi.-Hall(G) H -> pi.-Hall(f @* G) (f @* H).
proof: Proof. move=> sHD /and3P[sHG piH pi'GH]. by rewrite /pHall morphimS // morphim_pgroup // morphim_p_index. 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)