proposition: Lemma injmF gT rT (G D : {group gT}) (f : {morphism D >-> rT}) : 'injm f -> G \subset D -> f @* (F gT G) = F rT (f @* G).
proof: Proof. move=> injf sGD; have [sfGD injf'] := (morphimS f sGD, injm_invm injf). apply/esym/eqP; rewrite eqEsubset -(injmSK injf') ?gFsub_trans //. by rewrite !(subset_trans (injmF_sub _ _)) ?morphim_invm // gFsub_trans. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)