proposition: Lemma gFisom gT rT (G D : {group gT}) R (f : {morphism D >-> rT}) : G \subset D -> isom G (gval R) f -> isom (F gT G) (F rT R) f.
proof: Proof. case/(restrmP f)=> g [gf _ _ _]; rewrite -{f}gf => /isomP[injg <-]. by rewrite sub_isom ?gFsub ?injmF. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)