proposition: Lemma induced_path (G : sgraph) (S : {set G}) (x y : induced S) (p : seq (induced S)) : pathp x y p -> @pathp G (val x) (val y) (map val p).
proof: Proof. elim: p x => /= [|z p IH] x pth_p. - by rewrite (pathp_nil pth_p) pathpxx. - rewrite !pathp_cons in pth_p *. case/andP : pth_p => p1 p2. apply/andP; split => //. exact: IH. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)