proposition: Lemma prod_types_out (i : 'I_n) (A B : prod_types) : i \notin I -> A i = B i.
proof: Proof. move=> Hi. move: (A i) (B i). by rewrite (negbTE Hi) => -[] []. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba