proposition: Lemma filter_rcons s x : filter (rcons s x) = if a x then rcons (filter s) x else filter s.
proof: Proof. by rewrite -!cats1 filter_cat /=; case (a x); rewrite /= ?cats0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)