proposition: Lemma morphimS A B : A \subset B -> f @* A \subset f @* B.
proof: Proof. by move=> sAB; rewrite imsetS ?setIS. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)