proposition: Lemma idx_catL (x y z u v : G) (p : Path x y) (q : Path y z) : u \in p -> v \in p -> idx (pcat p q) u <= idx (pcat p q) v = (idx p u <= idx p v).
proof: Proof. move=> u_p v_p. rewrite /idx (nodesE (pcat _ _)) (lock index)/= -lock. by rewrite -cat_cons -nodesE !index_cat u_p v_p. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)