proposition: Lemma splitL x y (p : Path x y) : x != y -> exists z xz (p' : Path z y), p = pcat (edgep xz) p' /\ p' =i tail p.
proof: Proof. move => xy. case: p => p. elim: p x xy => [|a p IH] x xy H. - move/pathp_nil : (H) => ?. subst y. by rewrite eqxx in xy. - move: (H) => H'. move: H. rewrite pathp_cons => /andP [A B]. exists a. exists A. exists (Build_Path B). split; first exact: val_inj. move => w. by rewrite in_collective nodesE !inE. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)