proposition: Lemma pairwise_indeE : pairwise_inde <-> (forall i j, i != j -> inde_events d (E i) (E j)).
proof: Proof. split => [pi i j ij|]. red in pi. red in pi. have /pi : (#|[set i; j]| <= 2)%nat by rewrite cards2 ij. rewrite bigcap_setU !big_set1 => H. rewrite /inde_events H (big_setD1 i) ?inE ?eqxx ?orTb //= setU1K ?inE//. by rewrite big_set1. move=> H s. move sn : (#| s |) => n. case: n sn => [|[|[|//]]]. by move/eqP; rewrite cards_eq0 => /eqP ->{s} _; rewrite !big_set0 Pr_setT. by move/eqP/cards1P => [i ->{s}] _; rewrite !big_set1. move/eqP; rewrite cards2P => /existsP[a /existsP[b /andP[/eqP ->{s} ab]]] _. rewrite !bigcap_setU !big_set1 (big_setD1 a) ?inE ?eqxx ?orTb //=. by rewrite setU1K ?inE // big_set1 H. 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