proposition: Lemma inverse_Vis f x: bijection f -> inc x (target f) -> inc (Vf (inverse_fun f) x) (source f).
proof: Proof. move=> bf xt. have -> : source f= (target (inverse_fun f)) by aw. apply: Vf_target; aw;trivial; apply: (proj1(proj1(inverse_bij_fb bf))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)