proposition: Lemma fsdistjoin1 (A : choiceType) (D : {dist (FSDist_choiceType A)}) : fsdistjoin (fsdist1 D) = D.
proof: Proof. apply/fsdist_ext => d. by rewrite fsdistjoinE supp_fsdist1 big_imfset // big_seq1 fsdist1xx mul1R. 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