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