proposition: Lemma morphim_p_index pi G H : H \subset D -> pi.-nat #|G : H| -> pi.-nat #|f @* G : f @* H|.
proof: Proof. by move=> sHD; apply: pnat_dvd; rewrite index_morphim ?subIset // sHD orbT. 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)