proposition: Lemma sum_count_mem (T : finType) (P : pred T) l : \sum_(i | P i) (count_mem i) l = count P l.
proof: Proof. rewrite uniq_sum_count_mem; last exact: index_enum_uniq. by apply: eq_count => x /=; rewrite mem_index_enum. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools