proposition: Lemma E_sum_2 : X \= X1 @+ X2 -> `E X = `E X1 + `E X2.
proof: Proof. move=> Hsum; transitivity (\sum_(ta in 'rV[A]_n.+2) (X1 (ta ``_ ord0) * P ta + X2 (rbehead ta) * P ta)). by apply eq_bigr => ta _; rewrite Hsum mulRDl. rewrite big_split => //=; congr (_ + _). - transitivity (\sum_(a in A) (X1 a * \sum_(ta in 'rV_n.+1) (fdist_prod_of_rV P (a, ta)))). + rewrite -(big_rV_cons_behead _ xpredT xpredT); apply eq_bigr => a _. rewrite big_distrr /=; apply eq_bigr => i _. by rewrite row_mx_row_ord0 fdist_prod_of_rVE. + by apply eq_bigr => a _; rewrite fdist_fstE. - transitivity (\sum_(ta in 'rV_n.+1) (X2 ta * \sum_(a in A) (fdist_prod_of_rV P (a, ta)))). + rewrite -(big_rV_cons_behead _ xpredT xpredT) exchange_big /=. apply eq_bigr => ta _; rewrite big_distrr /=. by apply eq_bigr => a _; rewrite rbehead_row_mx fdist_prod_of_rVE. + by apply eq_bigr => ta _; rewrite fdist_sndE. 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