proposition: Lemma split_at_first_aux {A : pred D} x y (p : seq D) k : pathp x y p -> k \in A -> k \in x::p -> exists z p1 p2, [/\ p = p1 ++ p2, pathp x z p1, pathp z y p2, z \in A & forall z', z' \in A -> z' \in x::p1 -> z' = z].
proof: Proof. move => pth_p in_A in_p. pose n := find A (x::p). pose p1 := take n p. pose p2 := drop n p. pose z := last x p1. have def_p : p = p1 ++ p2 by rewrite cat_take_drop. move: pth_p. rewrite {1}def_p pathp_cat. case/andP => pth_p1 pth_p2. have X : has A (x::p) by apply/hasP; exists k. exists z. exists p1. exists p2. split => //. - suff -> : z = nth x (x :: p) (find A (x :: p)) by exact: nth_find. rewrite /z /p1 last_take // /n -ltnS. by rewrite has_find in X. - move => z' in_A' in_p'. have has_p1 : has A (x::p1) by (apply/hasP;exists z'). rewrite /z (last_nth x) -[z'](nth_index x in_p'). suff -> : index z' (x::p1) = size p1 by []. apply/eqP. rewrite eqn_leq. apply/andP;split. + by rewrite -ltnS -[(size p1).+1]/(size (x::p1)) index_mem. + rewrite leqNgt. apply: contraTN in_A' => C. rewrite -[z'](nth_index x in_p') unfold_in before_find //. apply: leq_trans C _. have -> : find A (x :: p1) = n by rewrite /n def_p -cat_cons find_cat has_p1. rewrite size_take. by case: (ltngtP n (size p)) => [|/ltnW|->]. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)