proposition: Lemma split_at_last {A : pred G} (x y : G) (p : Path x y) (k : G) : k \in A -> k \in p -> exists (z : G) (p1 : Path x z) (p2 : Path z y), [/\ p = pcat p1 p2, z \in A & forall z' : G, z' \in A -> z' \in p2 -> z' = z].
proof: Proof. move => kA kp. rewrite -mem_prev in kp. case: (split_at_first kA kp) => z [p1] [p2] [E zA I]. exists z. exists (prev p2). exists (prev p1). rewrite -prev_cat -E prevK. split => // z'. rewrite mem_prev. exact: I. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)