proposition: Lemma idx_mem x y (p : Path x y) z : z \in p -> idx p z <= size (tail p).
proof: Proof. case: p => p pth_p. rewrite /idx /irred in_collective nodesE inE /=. case: ifP => // E. rewrite eq_sym E /= -index_mem => H. exact: leq_trans H _. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)