proposition: Lemma fsdist_suppD1 (C : choiceType) (d : {dist C}) (x : C) : \sum_(i <- finsupp d `\ x) d i = (d x).~.
proof: Proof. rewrite -subR_eq0. rewrite RminusE subr_onem -RplusE -RoppE -R1E addR_opp -RplusE. case/boolP: (x \in finsupp d)=> xfd. by rewrite addRC -big_fsetD1 //= FSDist.f1 subRR. by rewrite fsfun_dflt // mem_fsetD1 // FSDist.f1 addR0 subRR. 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