proposition: Lemma mutual_indeE : mutual_inde <-> (forall J : {set I}, J \subset I -> Pr d (\bigcap_(i in J) E i) = \prod_(i in J) Pr d (E i)).
proof: Proof. rewrite /mutual_inde; split => [H J JI|H k J JI]. have [->{J JI}|J0] := eqVneq J set0. by rewrite !big_set0 Pr_setT. by rewrite (H #|J|.-1) ?prednK // card_gt0. by rewrite H //; apply/subsetP => i ij; rewrite inE. 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