proposition: Lemma inde_events_cplt (E F : {set A}) : inde_events E F -> inde_events E (~: F).
proof: Proof. rewrite /inde_events => EF; have : Pr d E = Pr d (E :&: F) + Pr d (E :&: ~:F). rewrite (total_prob d E (fun b => if b then F else ~:F)) /=; last 2 first. move=> i j ij; rewrite -setI_eq0. by case: ifPn ij => Hi; case: ifPn => //= Hj _; rewrite ?setICr // setIC setICr. by rewrite cover_imset big_bool /= setUC setUCr. by rewrite big_bool addRC. by rewrite addRC -subR_eq EF -{1}(mulR1 (Pr d E)) -mulRBr -Pr_of_cplt. 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