proposition: Lemma image_by_fun_injective f u v: injection f -> sub u (source f) -> sub v (source f) -> Vfs f u = Vfs f v -> u = v.
proof: Proof. move=> [ff injf]; move: u v. have aux: forall u v, sub u (source f) -> sub v (source f) -> Vfs f u = Vfs f v -> sub u v. move=> u v usf vsf aux t tu. have : inc (Vf f t) (Vfs f u) by apply /(Vf_image_P ff usf); ex_tac. rewrite aux;move /(Vf_image_P ff vsf)=> [w wv sf]. by rewrite (injf _ _ (usf _ tu) (vsf _ wv) sf). move=> u v usf vsf auw; apply: extensionality; apply: aux =>//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)