proposition: Lemma index_inj (T : eqType) (s : seq T) : {in s &, injective (index^~ s)}.
proof: Proof. by move => u v u_s v_s E; rewrite -[u](nth_index u u_s) E nth_index. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)