proposition: Lemma hasPIn (s : seq T) : reflect (exists2 x, x \In s & p x) (has p s).
proof: Proof. elim: s => [|y s IHs] /=; first by right; case. case Py: (p y); first by left; exists y=>//; apply/In_cons; left. apply: (iffP IHs)=>[] [x ysx Px]; exists x => //; first by apply/In_cons; right. by case/In_cons: ysx Px Py=>[->->|]. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)