proposition: Lemma prod_types_neq (A B : prod_types) : A != B -> exists i, (i \in I) && (A i != B i).
proof: Proof. move=> AB. case /boolP: [forall i, A i == B i]. move/forallP => /= AB'. elim: (negP AB). apply/eqP/ffunP => /= x. by apply/eqP. rewrite negb_forall => /existsP [x Hx]. exists x. rewrite Hx. case/boolP: (x \in I) => //= xe. elim: (negP Hx). move: (A x) (B x) {AB Hx} => /=. by rewrite (negbTE xe) => -[] []. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba