proposition: Lemma Convn_of_fsdistjoin (A : choiceType) (D : {dist {dist A}}) : Convn_of_fsdist D = fsdistjoin D.
proof: Proof. apply: fsdist_ext => a; rewrite -[LHS]Scaled1RK. rewrite (S1_proj_Convn_finType [the {affine _ -> _} of fsdist_eval a]). rewrite big_scaleR fsdistjoinE big_seq_fsetE; apply eq_bigr => -[d dD] _. by rewrite (scaleR_scalept _ (fdist_Rge0 _ _)) fdist_of_fsE Scaled1RK. 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