proposition: Lemma Ex_cEx : `E X = \sum_(i in I) `E_[X | F i] * Pr P (F i).
proof: Proof. apply/esym; rewrite /cEx. evar (f : I -> R); rewrite (eq_bigr f); last first. move=> i _; rewrite big_distrl /f; reflexivity. rewrite {}/f /= (bigID (fun i => Pr P (F i) != 0)) /=. rewrite [in X in _ + X = _]big1 ?addR0; last first. move=> i; rewrite negbK => /eqP ->; rewrite big1 // => r _; by rewrite mulR0. transitivity (\sum_(i in I | Pr P (F i) != 0) \sum_(j <- fin_img X) (j * Pr P (finset (X @^-1 j) :&: F i))). apply eq_bigr => i Fi0; apply eq_bigr => r _. by rewrite -!mulRA mulVR // mulR1. rewrite -Ex_altE /Ex_alt exchange_big /=; apply eq_bigr => r _. rewrite -big_distrr /=; congr (_ * _). transitivity (\sum_(i in I) Pr P (finset (X @^-1 r) :&: F i)). rewrite big_mkcond /=; apply eq_bigr => i _. case: ifPn => //; rewrite negbK => /eqP PFi0. rewrite /Pr big1 // => u; rewrite inE => /andP[uXr uFi]. move/eqP : PFi0; rewrite psumr_eq0// => /allP/(_ u). by rewrite mem_index_enum uFi implyTb => /(_ isT)/eqP. rewrite -Boole_eq; last first. move=> i j ij; rewrite -setI_eq0; apply/eqP/setP => u; rewrite !inE. apply/negbTE; rewrite !negb_and. have [/= Xur|//] := eqVneq (X u) r. move: (dis ij); rewrite -setI_eq0 => /eqP/setP/(_ u). by rewrite !inE => /negbT; rewrite negb_and. rewrite pr_eqE; congr Pr. move: cov; rewrite cover_imset => cov'. by rewrite -big_distrr /= cov' setIT. 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