proposition: Lemma E_SumIndCap n (S : 'I_n -> {set A}) k : `E (SumIndCap S k : {RV P -> R}) = SumPrCap S k.
proof: Proof. rewrite /SumIndCap /SumPrCap E_sumR; apply: eq_bigr => i Hi. by rewrite E_Ind. 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