proposition: Lemma path_to_induced (G : diGraph) (S : {set G}) (x y : induced S) p' : @pathp G (val x) (val y) p' -> {subset p' <= S} -> exists2 p, pathp x y p & p' = map val p.
proof: Proof. move=> pth_p' sub_p'. case: (lift_pathp _ _ pth_p' _) => //. - move=> z /sub_p' z_S. by apply/codomP; exists (Sub z z_S). - move=> p [pth_p /esym eq_p']. by exists p. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)