proposition: Lemma tnthP (t : n.-tuple T) x : reflect (exists i, x = tnth t i) (x \in t).
proof: Proof. apply: (iffP idP) => [/(nthP x)[i ltin <-] | [i ->]]; last exact: mem_tnth. by rewrite size_tuple in ltin; exists (Ordinal ltin); rewrite (tnth_nth x). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype path)