proposition: Lemma tnth_uniq (T : eqType) n (t : n.-tuple T) (i j : 'I_n) : uniq t -> (tnth t i == tnth t j) = (i == j).
proof: Proof. move => uniq_t. rewrite /tnth (set_nth_default (tnth_default t j)) ?size_tuple ?ltn_ord //. by rewrite nth_uniq // size_tuple ltn_ord. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)