proposition: Lemma filter_swap {A} (s : seq A) p1 p2 : filter p1 (filter p2 s) = filter p2 (filter p1 s).
proof: Proof. by rewrite -!filter_predI filter_predIC. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)