proposition: Lemma subset_imsetK (T1 T2 : finType) (f : T1 -> T2) (s t : {set T1}): injective f -> f @: s \subset f @: t -> s \subset t.
proof: Proof. move=> f_inj /subsetP H. by apply/subsetP => x /(imset_f f) /(H _) /imsetP[y Hy /f_inj ->]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)