proposition: Lemma perm_filter s1 s2 a : perm_eq s1 s2 -> perm_eq (filter a s1) (filter a s2).
proof: Proof. by move/permP=> s12_count; apply/permP=> Q; rewrite !count_filter. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)