proposition: Lemma inverse_V2 f y: bijection f -> inc y (source f) -> Vf (inverse_fun f) (Vf f y) = y.
proof: Proof. move=> bf ys. have yt: inc y (target (inverse_fun f)) by aw. move: (inverse_V (inverse_bij_fb bf) yt). by rewrite (ifun_involutive (proj1 (proj1 bf))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)