proposition: Lemma cinde_eventsC A (Q : fdist _ A) (E F G : {set A}) : cinde_events Q E F G -> cinde_events Q F E G.
proof: Proof. rewrite /cinde_events => Hef; by rewrite setIC mulRC. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba