proposition: Lemma allPnIn (s : seq T) : reflect (exists2 x, x \In s & ~~ p x) (~~ all p s).
proof: Proof. elim: s => [|x s IHs] /=; first by constructor=> [[x Hx _]]. rewrite /= andbC negb_and; case: IHs => IHs /=. - by constructor; case: IHs => y Hy Hay; exists y=>//; apply/In_cons; right. apply: (iffP idP) => [|[y]]; first by exists x=>//; apply/In_cons; left. by case/In_cons=>[->//|H1 H2]; elim: IHs; exists y. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)