proposition: Lemma triangular_laws_left0 (d : {dist C}) : Convn_of_fsdist (fsdistmap (@fsdist1 C) d) = d.
proof: Proof. apply: fsdist_ext => x; apply S1_inj. rewrite (S1_proj_Convn_finType [the {affine _ -> _} of fsdist_eval x]). under eq_bigr do rewrite fdist_of_fsE. rewrite (ssum_seq_finsuppE'' (fun i : {dist C} => i x)). rewrite supp_fsdistmap. rewrite big_imfset /=; last by move=> *; apply: fsdist1_inj. under eq_bigr do rewrite fsdist1E inE fsdist1map. have nx0 : \ssum_(i <- finsupp d `\ x) scalept (d i) (S1 (if x == i then 1 else 0)) = scalept (d x).~ (S1 0). transitivity (scalept (\sum_(i <- finsupp d `\ x) (d i)) (S1 0)). rewrite big_scaleptl' //; last by rewrite scale0pt. by apply: eq_fbigr => y /fsetD1P []; rewrite eq_sym=> /negbTE ->. by congr (_ _ _); rewrite fsdist_suppD1. case/boolP : (x \in finsupp d) => xfd. rewrite (big_fsetD1 x) //= nx0 eqxx -convptE -affine_conv/=. by rewrite avgRE mulR0 addR0 mulR1. by rewrite -(mem_fsetD1 xfd) nx0 fsfun_dflt // onem0 scale1pt. 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