proposition: Lemma path_xset_xedge x y (s : pred V) : gconnect x y -> x \in s -> y \notin s -> exists x' y', [/\ x' \in s, y' \notin s, gconnect x x', edge x' y' & gconnect y' y].
proof: Proof. move=> /connectP [p path_xp ->] xs yNs. pose n := find (predC s) p. have hasNs_p : has (predC s) p. apply/hasP; exists (last x p) => //=. have := mem_last x p; rewrite in_cons => /predU1P [eq_x|//]. by rewrite eq_x xs in yNs. have n_small : n < size p by rewrite -has_find. exists (nth x (x :: p) n), (nth x p n). rewrite [_ \notin s](@nth_find _ _ (predC s)) ?(pathP _ _) //. have [->|n_gt0] := posnP n. rewrite ?nth0 /= xs connect0; split=> //. by case: (p) yNs path_xp => [|? ? _ /andP[]]; rewrite //= xs. case: p {yNs n hasNs_p n_small} path_xp => //= z p. by move=> /andP [xz zp]; rewrite (appP connectP idP) //; exists p. rewrite -{1 2}[n]prednK //= -[_ \in s]negbK. rewrite [_ \notin s](@before_find _ _ (predC s)) ?prednK //=. split=> //. - apply/connectP; exists (take n p). by move: path_xp; rewrite -{1}[p](@cat_take_drop n) cat_path=> /andP[]. rewrite (last_nth x) size_take n_small. by case: (n) n_gt0 => //= k _; rewrite nth_take. - by have /pathP/(_ _ n_small) := path_xp => /(_ x). apply/connectP; exists (drop n.+1 p). move: path_xp; rewrite -{1}[p](@cat_take_drop n.+1) cat_path=> /andP[_]. rewrite (last_nth x) /= size_take ltn_neqAle n_small andbT. by have [->|] := altP eqP; rewrite /= ?drop_size ?nth_take. rewrite !(last_nth x) size_drop. move: n_small; rewrite leq_eqVlt => /predU1P[<-|]; rewrite ?subnn //. case: (size p) => //= - [|k] //; rewrite !ltnS => n_small. by rewrite subSS subSn // [RHS]/= nth_drop addSn subnKC. Qed.
imports: mathcomp(all_ssreflect) extra