proposition: Lemma idx_inj : {in nodes p, injective (idx p) }.
proof: Proof. move => u in_s v E. rewrite /idx in E. have A : v \in nodes p. by rewrite -index_mem -E index_mem. by rewrite -(nth_index x in_s) E nth_index. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)