proposition: Lemma connected_path (G : sgraph) (x y : G) (p : Path x y) : connected [set z in p].
proof: Proof. apply: (@connected_center _ x); last by rewrite inE. move => z. rewrite inE => A. case/psplitP : _ / A => {p} p1 p2. apply: (connectRI p1) => u Hu. by rewrite inE mem_pcat Hu. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)