proposition: Lemma injmF_sub gT rT (G D : {group gT}) (f : {morphism D >-> rT}) : 'injm f -> G \subset D -> f @* (F gT G) \subset F rT (f @* G).
proof: Proof. move=> injf sGD; have:= gFiso_cont (injm_restrm sGD injf). by rewrite im_restrm morphim_restrm (setIidPr _) ?gFsub. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)