proposition: Lemma idx_catR (x y z u v : G) (p : Path x y) (q : Path y z) : u \notin p -> v \notin p -> idx (pcat p q) u <= idx (pcat p q) v = (idx q u <= idx q v).
proof: Proof. move=> uNp vNp. rewrite /idx (nodesE (pcat _ _)) (lock index)/= -lock. rewrite -cat_cons lastI cat_rcons path_last -nodesE !index_cat. have /negbTE-> : u \notin belast x (val p). { apply: contraNN uNp. by rewrite mem_path nodesE lastI mem_rcons inE =>->. } have /negbTE-> : v \notin belast x (val p). { apply: contraNN vNp. by rewrite mem_path nodesE lastI mem_rcons inE =>->. } by rewrite leq_add2l. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)