proposition: Lemma usplitP z x y p : z \in x :: p -> upath x y p -> usplit z x y p.
proof: Proof. move => in_p /andP [U P]. case: (ppsplitP in_p P) U => p1 p2 sp1 sp2. rewrite -cat_cons cat_uniq -disjoint_has disjoint_sym => /and3P [? C ?]. suff H: z \notin p2 by constructor. apply/negP. apply: disjointE C _. by rewrite -(pathp_last sp1) // mem_last. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)