proposition: Lemma seq_tnthP (s : seq T) x : x \in s -> {i | x = tnth (in_tuple s) i}.
proof: Proof. move=> s_x; pose i := index x s; have lt_i: i < size s by rewrite index_mem. by exists (Ordinal lt_i); rewrite (tnth_nth x) nth_index. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype path)