proposition: Lemma splitR x y (p : Path x y) : x != y -> exists z (p' : Path x z) zy, p = pcat p' (edgep zy).
proof: Proof. move => xy. case: p. elim/last_ind => [|p a IH] H. - move/pathp_nil : (H) => ?. subst y. by rewrite eqxx in xy. - move: (H) => H'. case/andP : H. rewrite rcons_path => /andP [A B] C. have sP : pathp x (last x p) p by rewrite /pathp A eqxx. move: (pathp_rcons H') => ?; subst a. exists (last x p). exists (Build_Path sP). exists B. apply: val_inj => /=. by rewrite cats1. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)