proposition: Lemma idx_srev a x y (p : Path x y) : a \in p -> irred p -> idx (prev p) a = size (pval p) - idx p a.
proof: Proof. move => A B. rewrite /idx /prev !nodesE SubK /srev. case/andP: (valP p) => p1 /eqP p2. by rewrite -rev_rcons -[X in rcons _ X]p2 -lastI index_rev // -?nodesE -?irredE. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)