proposition: Lemma split_at_first {A : pred D} x y (p : Path x y) k : k \in A -> k \in p -> exists z (p1 : Path x z) (p2 : Path z y), [/\ p = pcat p1 p2, z \in A & forall z', z' \in A -> z' \in p1 -> z' = z].
proof: Proof. case: p => p pth_p /= kA kp. rewrite mem_path nodesE in kp. case: (split_at_first_aux pth_p kA kp) => z [p1] [p2] [def_p pth_p1 pth_p2 A1 A2]. exists z. exists (Build_Path pth_p1). exists (Build_Path pth_p2). split => //. + subst p. exact: val_inj. + move => ?. rewrite mem_path nodesE. exact: A2. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)