proposition: Lemma sub_isom (A : {set aT}) (C : {set rT}) : A \subset G -> f @* A = C -> 'injm f -> isom A C f.
proof: Proof. move=> sAG; case: (restrmP f sAG) => g [_ _ _ img] <-{C} injf. rewrite /isom -morphimEsub ?morphimDG ?morphim1 //. by rewrite subDset setUC subsetU ?sAG. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)