proposition: Lemma V_sum_n : forall n (X : {RV (P `^ n) -> R}) (Xs : 'rV[{RV P -> R}]_n), X \=sum Xs -> forall sigma2, (forall i, `V (Xs ``_ i) = sigma2) -> `V X = n%:R * sigma2.
proof: Proof. elim=> [X Xs X_Xs sigma2 Hsigma2|]. by inversion X_Xs. case=> [_ | n IH] Xsum Xs Hsum s Hs. - inversion Hsum. apply Eqdep_dec.inj_pair2_eq_dec in H; last exact eq_nat_dec. apply Eqdep_dec.inj_pair2_eq_dec in H0; last exact eq_nat_dec. subst Xs Xsum. by rewrite Var_cast_RV_fdist_rV1 mul1R. - move: Hsum; inversion 1. 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 Z n0 Xs. move: {IH}(IH Y _ H2) => IH. rewrite S_INR mulRDl -IH. + rewrite mul1R addRC (V_sum_2 H3) //; last exact: prod_dist_inde_rv_vec. by rewrite -(Hs ord0) /= row_mx_row_ord0 // head_of_fdist_rV_fdist_rV tail_of_fdist_rV_fdist_rV. + move=> i; rewrite -(Hs (lift ord0 i)). congr (`V _). rewrite (_ : lift _ _ = rshift 1 i); last exact: val_inj. by rewrite (@row_mxEr _ _ 1). 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