proposition: Theorem Pr_bigcup_incl_excl n (S : 'I_n -> {set A}) : Pr P (\bigcup_(i < n) S i) = \sum_(1 <= k < n.+1) ((-1)^(k-1) * SumPrCap S k).
proof: Proof. rewrite -E_Ind /=. rewrite /Ex. erewrite eq_bigr. 2: by move=> ? _; rewrite /= Ind_bigcup_incl_excl. simpl. erewrite eq_bigr. 2: by move=> a Ha; rewrite big_distrl. rewrite exchange_big /=. apply: eq_bigr => i _. by rewrite -E_SumIndCap -E_scalel_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