proposition: Lemma Path_to_induced (G : sgraph) (S : {set G}) (x y : induced S) (p : Path (val x) (val y)) : {subset p <= S} -> exists q : Path x y, map val (nodes q) = nodes p.
proof: Proof. case: p => p pth_p sub_p. case: (path_to_induced pth_p). - move=> z z_p; apply: sub_p. by rewrite mem_path nodesE /= inE z_p. - move=> q pth_q eq_p. exists (Sub q pth_q). by rewrite !nodesE /= eq_p. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)