proposition: Lemma Ex_altE : Ex_alt = `E X.
proof: Proof. rewrite /Ex. transitivity (\sum_(r <- fin_img X) \sum_(u in U | X u == r) (X u * P u)). apply eq_bigr => /= r _; rewrite pr_eqE big_distrr /=. by apply eq_big => //= a; rewrite !inE // => /eqP ->. by rewrite -partition_big_fin_img. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct reals) Reals Lra ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist