proposition: Lemma psplitP z x y (p : Path x y) : z \in p -> psplit z p.
proof: Proof. move: (valP p) => pth_p in_p. rewrite mem_path nodesE in in_p. case/(ppsplitP in_p) E : _ / pth_p => [p1 p2 P1 P2]. have -> : p = pcat (Sub p1 P1) (Sub p2 P2) by exact: val_inj. by constructor. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)