proposition: Lemma set_vals_prod_vals_join (I J : {set 'I_n}) vals vals' : set_vals (prod_vals I vals) (set_vals (prod_vals J vals) vals') = set_vals (prod_vals (I :|: J) vals) vals'.
proof: Proof. apply/ffunP => i. case/boolP: (i \in I) => iI. by rewrite !set_vals_prod_vals // inE iI. rewrite set_vals_tl //. case/boolP: (i \in J) => iJ. by rewrite !set_vals_prod_vals // inE iJ orbT. by rewrite !set_vals_tl // inE negb_or iI. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba