proposition: Lemma char_injm (G H : {group aT}) : G \subset D -> H \subset D -> (f @* H \char f @* G) = (H \char G).
proof: Proof. move=> sGD sHD; apply/idP/idP; last exact: injm_char. by move/(injm_char (injm_invm injf)); rewrite !morphim_invm ?morphimS // => ->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)