proposition: Lemma right_i_V f s x: is_right_inverse f s -> inc x (target f) -> Vf f (Vf s x) = x.
proof: Proof. move=> rsf xtf; move: (xtf);rewrite - (right_i_source rsf). by move: rsf=> [csf c] xs;rewrite - compfV // c; bw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)