proposition: Lemma direct_inv_im f y: function f -> sub y (target f) -> sub (Vfs f (Vfs (inverse_fun f) y)) y.
proof: Proof. move=> ff yt x. have aux: sub (Vfs (inverse_fun f) y) (source f). by rewrite /inverse_fun/Vfs; aw; apply: sub_inv_im_source. move/(Vf_image_P ff aux) =>[u /dirim_P [z zy /igraph_pP]]. by rewrite - ifun_g (ifun_involutive ff) => xx ->; rewrite -(Vf_pr ff xx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)