proposition: Lemma cinde_preimC (e f g : {set 'I_n}) : cinde_preim e f g -> cinde_preim f e g.
proof: Proof. move=> Hef vals; exact: cinde_eventsC. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba