proposition: Lemma cinde_preim_inter e f g : cinde_preim e f g -> cinde_preim (e :&: f) (e :&: f) g.
proof: Proof. move=> Hp. have Hp2 : cinde_preim (e :\: (e :\: f :\: g)) f g. apply (@cinde_preim_sub e) => // ; apply/subsetP => j; by cases_in j. have : cinde_preim (e :\: (e :\: f :\: g)) (f :\: (f :\: e :\: g)) g. move/cinde_preimC in Hp2. apply/cinde_preimC. apply (@cinde_preim_sub f) => // ; apply/subsetP => j; by cases_in j. move=> {}Hp vals. move/(_ vals): Hp. rewrite /cinde_events /cPr /Pr -!preim_vars_inter. rewrite (_ : _ :|: g = (e :&: f) :|: g); last by apply/setP => j; cases_in j. rewrite 2!(_ : _ :\: _ :|: _ = (e :&: f) :|: g); try by apply/setP => j; cases_in j. by rewrite setUid. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba