proposition: Lemma hasPnIn (s : seq T) : reflect (forall x, x \In s -> ~~ p x) (~~ has p s).
proof: Proof. apply: (iffP (negPP (hasPIn s)))=>H. - by move=>x Hx; apply: contra_notN H=>Px; exists x. by case=>x Hx; apply/negP/H. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)