proposition: Lemma morphimSK A B : A \subset D -> (f @* A \subset f @* B) = (A \subset 'ker f * B).
proof: Proof. move=> sAD; transitivity (A \subset 'ker f * (D :&: B)). by rewrite -morphimK ?subsetIl // -sub_morphim_pre // /morphim setIA setIid. by rewrite setIC group_modl (subsetIl, subsetI) // andbC sAD. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)