proposition: Lemma nilp_filter (p : pred A) s : reflect {in s, forall z, ~~ p z} (nilp (filter p s)).
proof: Proof. case E : (nilp _); constructor. - move: E; rewrite nilp_hasPn=>/hasPn H x Kx; apply/negP=>Px. by move: (H x); rewrite mem_filter Px=>/(_ Kx). move=>X; move/negP: E; elim. rewrite nilp_hasPn; apply/negP=>/hasP [x]. rewrite mem_filter=>/andP [Px Kx] _. by move: (X x Kx); rewrite Px. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)