proposition: Lemma set_valsC I J (A : prod_types I) (B : prod_types J) V : [disjoint I & J] -> set_vals A (set_vals B V) = set_vals B (set_vals A V).
proof: Proof. move/setDidPl/setP => Disj. apply/ffunP => /= i. case/boolP: (i \in I) => iI. move: (Disj i); rewrite inE iI andbT => /set_vals_tl ->. by rewrite (set_vals_hd V). case/boolP: (i \in J) => iJ. by rewrite set_vals_tl //; apply set_vals_hd. by rewrite !set_vals_tl. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba