proposition: Lemma E_sumR I r p (Z : I -> {RV P -> R}) : `E (sumR_RV r p Z) = \sum_(i <- r | p i) (`E (Z i)).
proof: Proof. rewrite /Ex. erewrite eq_bigr. 2: by move=> a Ha; rewrite big_distrl. by rewrite exchange_big /=; apply: eq_bigr => i Hi. 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