proposition: Lemma inverse_V f x: bijection f -> inc x (target f) -> Vf f (Vf (inverse_fun f) x) = x.
proof: Proof. move=> bf xt; move:(bij_surj bf xt) => [y ys xv]; rewrite {2} xv. move:(bijective_inv_f bf)=> bif. congr Vf; symmetry; apply:(Vf_pr bif). rewrite ifun_g xv; apply/igraph_pP; Wtac; fct_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)