proposition: Lemma filter_rev a s : filter a (rev s) = rev (filter a s).
proof: Proof. by elim: s => //= x s IH; rewrite fun_if !rev_cons filter_rcons IH. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)