proposition: Lemma f1 : \sum_(a <- finsupp f) f a = 1.
proof: Proof. rewrite -(FSDist.f1 P) !big_seq_fsetE /=. have hP (a : [finType of finsupp P]) : a \in finsupp f. by rewrite mem_finsupp fsfunE ffunE inE -mem_finsupp fsvalP. pose h a := FSetSub (hP a). rewrite (reindex h) /=. by apply eq_bigr => i _; rewrite fsfunE ffunE inE. by exists (@fsval _ _) => //= -[a] *; exact: val_inj. 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