proposition: Lemma idx_nLR u : u \in nodes (pcat p q) -> idx (pcat p q) z < idx (pcat p q) u -> u \notin nodes p /\ u \in tail q.
proof: Proof. move => A B. rewrite -idxR // in B. by rewrite (disjointFl dis_pq B). Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)