proposition: Lemma prod_vals_eqP vals1 vals2 i : prod_vals vals1 i = prod_vals vals2 i <-> (i \in I -> vals1 i = vals2 i).
proof: Proof. split; rewrite !ffunE; case: (i \in I) (vals1 i) (vals2 i) => // v1 v2; exact. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba