proposition: Lemma filter_predI a1 a2 s : filter (predI a1 a2) s = filter a1 (filter a2 s).
proof: Proof. by elim: s => //= x s ->; rewrite andbC; case: (a2 x). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)