proposition: Lemma prod_vals_eq (vals1 vals2 : univ_types) i : (i \in I -> vals1 i = vals2 i) -> prod_vals vals1 i = prod_vals vals2 i.
proof: Proof. move=> Hi; exact/prod_vals_eqP. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba