fact: Definition kwide_inde := forall (J : {set I}), (#|J| <= k)%nat -> Pr d (\bigcap_(i in J) E i) = \prod_(i in J) Pr d (E i).
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