proposition: Lemma sum_fdist_supp (f : A -> R) d (P : pred A): \sum_(a in A | P a) d a * f a = \sum_(a | P a && (a \in fdist_supp d)) d a * f a.
proof: Proof. rewrite (bigID (mem (fdist_supp d))) /= addrC big1 ?add0r//. by move=> i; rewrite inE negbK => /andP[_ /eqP] ->; rewrite mul0r. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR logb realType_ext ssr_ext ssralg_ext bigop_ext