proposition: Lemma prod_vals_set_vals (A : prod_types) vals : prod_vals (set_vals A vals) = A.
proof: Proof. apply/ffunP => j. apply (set_vals_inj (vals := vals)). case/boolP: (j \in I) => Hj. by rewrite set_vals_prod_vals. 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