proposition: Lemma direct_inv_im_surjective f y: surjection f -> sub y (target f) -> Vfs f (Vfs (inverse_fun f) y) = y.
proof: Proof. move=> [ff sf] yt. apply: extensionality; first by apply: direct_inv_im. move=> x xs; rewrite -iim_fun_pr. apply/Vf_image_P =>//; first by apply: sub_inv_im_source. have [u us Jg] := (sf _ (yt _ xs)). exists u=>//;apply/iim_fun_P; ex_tac;rewrite Jg; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)