proposition: Lemma ppsplitP z x y p : z \in x :: p -> pathp x y p -> pathp_split z x y p.
proof: Proof. case/splitPl => p1 p2 /eqP H1 /andP [H2 H3]. rewrite cat_path last_cat in H2 H3. case/andP : H2 => H2 H2'. constructor; last rewrite -(eqP H1); exact/andP. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)