proposition: Lemma cinde_preim_ok (e f g : {set 'I_n}) : cinde_preim e f g <-> P |= prod_vars e _|_ prod_vars f | (prod_vars g).
proof: Proof. split. - move=> Hpreim. apply/cinde_rv_events => A B C. set vals := set_vals C (set_vals A (set_vals B vals0)). case /boolP: [forall i in e, vals i == set_vals A vals0 i]; last first. case: (cinde_events_vals A B C) => // /forallP Heg /negP; elim. apply/forallP => i; apply /implyP => Hie. case /boolP: (i \in g) => Hig; last by rewrite /vals set_vals_tl // (set_vals_hd vals0). rewrite /vals (set_vals_hd vals0) //. move/implyP: (Heg i); rewrite inE Hie; exact. move/forallP => /= He. have {}He x Hx := eqP (implyP (He x) Hx). case /boolP: [forall i in f, vals i == set_vals B vals0 i]. move/forallP => /= Hf. have {}Hf x Hx := eqP (implyP (Hf x) Hx). move: (Hpreim vals). rewrite (preim_vars_vals _ He) // (preim_vars_vals _ Hf) //. by rewrite /cinde_events -!preim_prod_vars -!preim_inter. move/cinde_preimC in Hpreim. move=> HB; apply cinde_eventsC. case: (cinde_events_vals B A C) HB => // /forallP Hfg. rewrite negb_forall => /existsP [i]. rewrite negb_imply /vals => /andP [Hif]. case /boolP: (i \in g) => Hig. move: (Hfg i); by rewrite inE Hif Hig /= (set_vals_hd vals0) // => ->. case /boolP: (i \in e) => Hie; last by rewrite set_vals_tl // set_vals_tl // eqxx. rewrite set_vals_tl // (set_vals_hd vals0) // => /eqP Hvi. apply/cinde_eventsC. move/cinde_preimC/cinde_preim_inter/(_ vals): Hpreim. rewrite {1}/cinde_events -!preim_vars_inter setUid /=. case/Rxx2. move/cPr_eq0/Pr_set0P => Hx. have HAC : Pr P (finset (prod_vars e @^-1 A) :&: finset (prod_vars g @^-1 C)) = 0. apply Pr_set0P => u Hu; apply Hx. rewrite -preim_vars_inter; apply/preim_varsP => j. move: Hu; rewrite !inE. rewrite /vals => /andP[] /eqP <- /eqP <-. case/boolP: (j \in g) => jg. by rewrite set_vals_prod_vars. case/boolP: (j \in e) => // je. by rewrite set_vals_tl // set_vals_prod_vars. rewrite /cinde_events (proj2 (cPr_eq0 _ _ _)). by rewrite (proj2 (cPr_eq0 _ _ _)) // mul0R. apply/Pr_set0P => u Hu. apply(proj1 (Pr_set0P _ _) HAC). move: Hu; by rewrite !inE => /andP[] /andP[] -> _ ->. exact: (cinde_events_cPr1 (i:=i)). - move=> Hdrv vals. move/cinde_rv_events: Hdrv. move/(_ (prod_vals e vals) (prod_vals f vals) (prod_vals g vals)). rewrite -(preim_vars_vals (prod_vals e vals) (set_vals_prod_vals _ vals)). rewrite -(preim_vars_vals (prod_vals f vals) (set_vals_prod_vals _ vals)). rewrite -(preim_vars_vals (prod_vals g vals) (set_vals_prod_vals _ vals)). by rewrite -!preim_prod_vars. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba