proposition: Lemma nthP (T : eqType) (s : seq T) x x0 : reflect (exists2 i, i < size s & nth x0 s i = x) (x \in s).
proof: Proof. apply: (iffP idP) => [|[n Hn <-]]; last exact: mem_nth. by exists (index x s); [rewrite index_mem | apply nth_index]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)