proposition: Lemma Pr_bigcup (B : finType) (p : pred B) F : Pr (\bigcup_(i | p i) F i) <= \sum_(i | p i) Pr (F i).
proof: Proof. rewrite /Pr; elim: (index_enum _) => [| h t IH]. by rewrite big_nil; apply/RleP/sumr_ge0 => b _; rewrite big_nil. rewrite big_cons; case: ifP => H1. apply: leR_trans; first by eapply leR_add2l; exact: IH. rewrite [X in _ <= X](exchange_big_dep (fun h => (h \in A) && [pred x in \bigcup_(i | p i) F i] h)) /=; last first. by move=> b a Ea jFi; apply/bigcupP; exists b. rewrite big_cons /= H1 big_const iter_addR -exchange_big_dep /=; last first. by move=> b a Ea iFj; apply/bigcupP; exists b. apply/leR_add2r. rewrite -{1}(mul1R (P h)); apply: (@leR_wpmul2r (P h)) => //. rewrite (_ : 1 = 1%:R) //; apply/le_INR/ssrnat.leP/card_gt0P. by case/bigcupP : H1 => b Eb hFb; exists b; rewrite -topredE /= Eb. apply/(leR_trans IH)/leR_sumR => b Eb; rewrite big_cons. case: ifPn => hFb; last by apply/RleP; rewrite lexx. by rewrite -[X in X <= _]add0R; exact/leR_add2r. 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