proposition: Lemma uniq_sum_count_mem (T : eqType) (P : pred T) l s : uniq s -> \sum_(i <- s | P i) (count_mem i) l = count (predI (mem s) P) l.
proof: Proof. move=> suniq; rewrite -big_filter -size_filter. have /eq_filter -> : predI (mem s) P =i [seq x <- s | P x]. by move=> i; rewrite inE mem_filter andbC. have {suniq} : uniq [seq x <- s | P x] by exact: filter_uniq. elim: filter => [_ | s0 {}s IHs]. by rewrite big_nil (eq_filter (a2 := pred0)); first by rewrite filter_pred0. rewrite big_cons => /= /andP[s0s {}/IHs ->]. rewrite !size_filter -[RHS]addn0. rewrite [in RHS](eq_count (a2 := predU (pred1 s0) (mem s))); first last. by move => i; rewrite /= in_cons. have /eq_count/(_ l) : predI (pred1 s0) (mem s) =1 pred0. move=> i /=; apply/negP => /andP[/eqP -> s0s']. by rewrite s0s' in s0s. rewrite count_pred0 => <-. by rewrite count_predUI. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)