proposition: Lemma has_nthP a s x0 : reflect (exists2 i, i < size s & a (nth x0 s i)) (has a s).
proof: Proof. elim: s => [|x s IHs] /=; first by right; case. case nax: (a x); first by left; exists 0. by apply: (iffP IHs) => [[i]|[[|i]]]; [exists i.+1 | rewrite nax | exists i]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)