proposition: Lemma sub_morphim_pre A R : A \subset D -> (f @* A \subset R) = (A \subset f @*^-1 R).
proof: Proof. move=> sAD; rewrite -morphpreSK (morphimS, morphimK) //. apply/idP/idP; first by apply: subset_trans; apply: mulG_subr. by move/(mulgS ('ker f)); rewrite -morphpreMl ?(sub1G, mul1g). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)