proposition: Lemma fsdistbind1 (A : choiceType) (p : {dist A}) : p >>= @fsdist1 A = p.
proof: Proof. apply/val_inj/val_inj => /=; congr fmap_of_fsfun; apply/fsfunP => b. rewrite fsdistbindEcond; case: ifPn => [|H]. case/bigfcupP => /= d; rewrite andbT. case/imfsetP => /= a ap ->{d}. rewrite supp_fsdist1 inE => /eqP ->{b}. rewrite (big_fsetD1 a) //= fsdist1xx mulR1 big1_fset ?addR0 // => a0. by rewrite !inE => /andP[aa0] a0p _; rewrite fsdist10 ?mulR0// eq_sym. have [->//|pb0] := eqVneq (p b) 0%coqR. case/bigfcupP : H. exists (fsdist1 b); last by rewrite supp_fsdist1 inE. by rewrite andbT; apply/imfsetP; exists b => //=; rewrite mem_finsupp. 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