proposition: Lemma set_vals_eq (A B : prod_types) vals i : set_vals A vals i == set_vals B vals i = (A i == B i) || (i \notin I).
proof: Proof. rewrite !ffunE. case: (i \in I) (A i) (B i) => a b. - by rewrite orbF. - by rewrite eqxx orbT. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba