proposition: Lemma E_sum_n : forall n (Xs : 'rV[{RV P -> R}]_n) (X : {RV (P `^ n) -> R}), X \=sum Xs -> `E X = \sum_(i < n) `E (Xs ``_ i).
proof: Proof. elim => [Xs Xbar | [_ Xs Xbar | n IHn Xs Xbar] ]. - by inversion 1. - inversion 1; subst. apply Eqdep_dec.inj_pair2_eq_dec in H0; last exact eq_nat_dec. apply Eqdep_dec.inj_pair2_eq_dec in H1; last exact eq_nat_dec. subst Xs Xbar. by rewrite big_ord_recl big_ord0 addR0 E_cast_RV_fdist_rV1. - inversion 1; subst. apply Eqdep_dec.inj_pair2_eq_dec in H1; last exact eq_nat_dec. apply Eqdep_dec.inj_pair2_eq_dec in H2; last exact eq_nat_dec. subst Z Xs. rewrite big_ord_recl. rewrite [X in _ = _ + X](_ : _ = \sum_(i < n.+1) `E (Xs0 ``_ i)); last first. apply eq_bigr => i _ /=. apply eq_bigr => a _ /=. rewrite (_ : lift _ _ = rshift 1 i); last exact: val_inj. by rewrite (@row_mxEr _ _ 1). rewrite -(IHn _ _ H3) (E_sum_2 H4) row_mx_row_ord0. by rewrite /Ex head_of_fdist_rV_fdist_rV tail_of_fdist_rV_fdist_rV. 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