proposition: Lemma idxR u : u \in pcat p q -> u \in tail q = z <[pcat p q] u.
proof: Proof. move => A. symmetry. rewrite /idx /pcat nodesE -cat_cons index_cat -nodesE path_end. rewrite index_cat mem_pcatT in A *. case/orP: A => A. - rewrite A (disjointFr dis_pq A). apply/negbTE. rewrite -leqNgt -!/(idx _ _) (idx_end irr_p) -ltnS. rewrite -index_mem in A. apply: leq_trans A _. by rewrite nodesE. - rewrite A (disjointFl dis_pq A) -!/(idx _ _) (idx_end irr_p). by rewrite nodesE /= addSn ltnS leq_addr. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)