proposition: Lemma filter_sub (p1 p2 : pred A) (s : seq A) : subpred p1 p2 -> {subset filter p1 s <= filter p2 s}.
proof: Proof. move=>S; rewrite (_ : filter p1 s = filter p1 (filter p2 s)). - by apply: mem_subseq; apply: filter_subseq. rewrite -filter_predI; apply: eq_in_filter=>x X /=. by case E : (p1 x)=>//=; rewrite (S _ E). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)