proposition: Lemma isom_isog (D : {group aT}) (f : {morphism D >-> rT}) : A \subset D -> isom f -> isog.
proof: Proof. move=> sAD isof; apply: (@misom_isog f); rewrite /misom isof andbT. by apply/morphicP; apply: (sub_in2 (subsetP sAD) (morphM f)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)