proposition: Lemma filter_nilP (p : pred A) xs : reflect (forall x, p x -> x \in xs -> false) ([seq x <- xs | p x] == [::]).
proof: Proof. case: eqP=>E; constructor. - move=>x H1 H2; suff : x \in [seq x <- xs | p x] by rewrite E. by rewrite mem_filter H1 H2. move=>H; apply: E; apply: size0nil; apply/eqP; rewrite size_filter. by rewrite eqn0Ngt -has_count; apply/hasPn=>x /H; case: (p x)=>//; apply. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)