proposition: Lemma fsdist_convE a : fsdist_conv a = d1 a <| p |> d2 a.
proof: Proof. rewrite /fsdist_conv -lock fsfunE. case: ifPn => //. rewrite /D; case: ifPn; [| case: ifPn]. - by move/eqP ->; rewrite conv0 mem_finsupp negbK => /eqP ->. - by move/eqP ->; rewrite conv1 mem_finsupp negbK => _ /eqP ->. - move=> _ _; rewrite inE !mem_finsupp negb_or !negbK => /andP [] /eqP -> /eqP ->. by rewrite convmm. 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