proposition: Lemma perm_filterC a s : perm_eql (filter a s ++ filter (predC a) s) s.
proof: Proof. apply/permPl; elim: s => //= x s IHs. by case: (a x); last rewrite /= -cat1s perm_catCA; rewrite perm_cons. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)