proposition: Lemma fdist_convE a : fdist_conv a = (p : R) * d1 a + (Prob.p p).~ * d2 a.
proof: Proof. rewrite /fdist_conv; unlock => /=. by rewrite fdist_convnE !big_ord_recl big_ord0 /= addr0 !fdistI2E. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR logb realType_ext ssr_ext ssralg_ext bigop_ext