proposition: Lemma injmSK A B : A \subset D -> (f @* A \subset f @* B) = (A \subset B).
proof: Proof. by move=> sAD; rewrite morphimSK // ker_injm mul1g. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)