proposition: Lemma E_id_rem_helper : X \= X1 @+ X2 -> P |= X1' _|_ X2' -> \sum_(i in 'rV[A]_n.+2) (X1 (i ``_ ord0) * X2 (rbehead i) * P i) = `E X1 * `E X2.
proof: Proof. move=> Hsum Hinde. rewrite -!Ex_altE. apply trans_eq with (\sum_(r <- undup (map X1 (enum A))) \sum_(r' <- undup (map X2 (enum ('rV[A]_n.+1)))) ( r * r' * @pr_eq _ _ P1 X1 r * @pr_eq _ _ P2 X2 r')); last first. rewrite [in RHS]big_distrl /=; apply eq_bigr => i _. rewrite big_distrr /=; apply eq_bigr => j _. by rewrite -!mulRA [in RHS](mulRCA _ j). rewrite -(big_rV_cons_behead _ xpredT xpredT) /=. apply trans_eq with (\sum_(a in A) \sum_(j in 'rV[A]_n.+1) (X1 a * X2 j * P (row_mx (\row_(k < 1) a) j))). apply eq_bigr => a _; apply eq_bigr => ta _. by rewrite row_mx_row_ord0 rbehead_row_mx. rewrite (partition_big_undup_map _ X1); last by rewrite /index_enum -enumT; apply enum_uniq. rewrite /index_enum -enumT. apply eq_bigr => /= r _. rewrite {1}enumT exchange_big /= (partition_big_undup_map _ X2); last first. by rewrite /index_enum -enumT; apply enum_uniq. rewrite /index_enum -enumT. apply eq_bigr => /= r' _. apply trans_eq with (r * r' * \sum_(i0 | X2 i0 == r') \sum_(i1 | X1 i1 == r) (P (row_mx (\row_(k < 1) i1) i0))). rewrite big_distrr /= /index_enum -!enumT; apply eq_bigr => ta ta_r'. rewrite big_distrr /=; apply eq_bigr => a a_l. move/eqP : ta_r' => <-. by move/eqP : a_l => <-. rewrite -[RHS]mulRA; congr (_ * _). rewrite exchange_big /=. have {}Hinde := Hinde r r'. have -> : `Pr[ X1 = r ] = `Pr[ X1' = r ]. rewrite 2!pr_eqE /P1 /head_of_fdist_rV Pr_fdist_fst Pr_fdist_prod_of_rV1; congr Pr. by apply/setP => /= v; rewrite !inE /X1'. have -> : `Pr[ X2 = r' ] = `Pr[ X2' = r' ]. rewrite 2!pr_eqE /P1 /tail_of_fdist_rV Pr_fdist_snd Pr_fdist_prod_of_rV2; congr Pr. by apply/setP => /= v; rewrite !inE /X2'. rewrite -Hinde. rewrite pr_eqE /ambient_dist /Pr. transitivity (\sum_(a : 'rV_n.+2 | (X1 (a ``_ ord0) == r) && (X2 (rbehead a) == r')) P a). by rewrite -(big_rV_cons_behead _ [pred x | X1 x == r] [pred x | X2 x == r']) /=. apply eq_bigl => /= v. by rewrite /X1' /X2' !inE /RV2 xpair_eqE. 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