proposition: Lemma set_vals_inj (A B : prod_types) vals i : set_vals A vals i = set_vals B vals i -> A i = B i.
proof: Proof. set goal := _ -> _. case/boolP: (i \in I) => Hi; subst goal. move/eqP; rewrite set_vals_eq orbC. by move: (A i) (B i); rewrite Hi => a b /= /eqP. move=> _; exact: prod_types_out. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba