proposition: Lemma Convn_of_fsdist1 (C : convType) (x : C) : Convn_of_fsdist (fsdist1 x) = x.
proof: Proof. apply: (@S1_inj _ _ x). rewrite S1_Convn_finType /=. rewrite (eq_bigr (fun=> S1 x)); last first. move=> i _; rewrite fdist_of_fsE fsdist1E /= -(supp_fsdist1 x). rewrite fsvalP scale1pt /=; congr (S1 _). by case: i => i /=; rewrite supp_fsdist1 inE => /eqP. by rewrite big_const (_ : #| _ | = 1%N) // -cardfE supp_fsdist1 cardfs1. 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