proposition: Lemma f1 : \sum_(b in A) f b = 1.
proof: Proof. rewrite -(FSDist.f1 P) (bigID (fun x => x \in finsupp P)) /=. rewrite [X in (_ + X = _)%coqR](_ : _ = 0) ?addR0. by rewrite big_uniq /= ?fset_uniq //; apply eq_bigr => i _; rewrite ffunE. by rewrite big1 // => a; rewrite mem_finsupp negbK ffunE => /eqP. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(finmap) Reals mathcomp(mathcomp_extra) mathcomp(classical_sets boolp cardinality Rstruct reals) mathcomp(ereal topology esum measure probability) ssrR realType_ext Reals_ext ssr_ext ssralg_ext bigop_ext fdist convex