proposition: Lemma idx_end x y (p : Path x y) : irred p -> idx p y = size (tail p).
proof: Proof. rewrite /irred nodesE => irr_p. by rewrite /idx nodesE -[in index _](path_last p) index_last. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)