proposition: Lemma supp_fsdistbind : finsupp fsdistbind = D.
proof: Proof. apply/fsetP => b; rewrite mem_finsupp; apply/idP/idP => [|]. by rewrite fsdistbindEcond; case: ifPn => //; rewrite eqxx. case/bigfcupP => dB. rewrite andbT => /imfsetP[a] /= ap ->{dB} bga. rewrite fsdistbindE. apply/eqP => H. have : p a * g a b <> 0. by rewrite mulR_eq0 => -[]; apply/eqP; rewrite -mem_finsupp. apply. move/eqP : H; rewrite psumr_eq0; last first. by move=> a0 _; rewrite RmultE mulr_ge0//; exact/RleP. by move=> /allP H; exact/eqP/H. 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