proposition: Lemma sum_fdist_binary_supp (f : A -> R) : \sum_(i in fdist_supp d) f i = f fdist_binary_supp0 + f fdist_binary_supp1.
proof: Proof. transitivity (\sum_(i <- enum (fdist_supp d)) f i); last first. by rewrite enum_fdist_binary_supp 2!big_cons big_nil addr0. by rewrite big_filter; apply eq_bigl => ?; rewrite !inE. 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