proposition: Lemma morphim_isom (H : {group aT}) (K : {group rT}) : H \subset G -> isom H K f -> f @* H = K.
proof: Proof. by case/(restrmP f)=> g [gf _ _ <- //]; rewrite -gf; case/isomP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)