proposition: Lemma Path_from_induced (G : sgraph) (S : {set G}) (x y : induced S) (p : Path x y) : { q : Path (val x) (val y) | {subset q <= S} & nodes q = map val (nodes p) }.
proof: Proof. case: p => p pth_p. exists (Build_Path (induced_path pth_p)); last by rewrite !nodesE. move=> z; rewrite mem_path nodesE /= -map_cons => /mapP[z' _ ->]; exact: valP. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)