proposition: Lemma cinde_preim_sub (e e' f g : {set 'I_n}) : e :&: (f :|: g) \subset e' -> e' \subset e -> cinde_preim e f g -> cinde_preim e' f g.
proof: Proof. rewrite /cinde_preim => ee' e'e Hef vals. have ee'g : (e :\: e') :&: g = set0. apply/setP => i; move/subsetP/(_ i): ee'; by cases_in i. transitivity (\sum_(A : Tfin_img (prod_vars (e :\: e'))) let v := set_vals (nth_fin_img A) vals in `Pr_P[preim_vars e v :&: preim_vars f v | preim_vars g v]). rewrite /cPr -!preim_vars_inter. have -> : e' :|: f :|: g = (e :|: f :|: g) :\: (e :\: e'). apply/setP => i. move/subsetP/(_ i): e'e. move/subsetP/(_ i): ee'. by cases_in i. rewrite Pr_preim_vars_sub; last by apply/subsetP=> i; cases_in i. rewrite /Rdiv big_distrl; apply eq_bigr => A _ /=. by rewrite -!preim_vars_inter (@preim_vars_set_vals_tl g). under eq_bigr => A _ /=. rewrite Hef (@preim_vars_set_vals_tl g) // (@preim_vars_set_vals_tl f). over. apply/setP => i; move/subsetP/(_ i): ee'; by cases_in i. rewrite -2!big_distrl /=. congr (_ / _ * _). rewrite -preim_vars_inter. have -> : e' :|: g = (e :|: g) :\: (e :\: e'). apply/setP => i. move/subsetP/(_ i): e'e. move/subsetP/(_ i): ee'. by cases_in i. rewrite Pr_preim_vars_sub; last by apply/subsetP=> i; cases_in i. apply eq_bigr => A _. by rewrite preim_vars_inter (@preim_vars_set_vals_tl g) //. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba