proposition: Lemma preim_varsP (I : {set 'I_n}) vals u : reflect (forall i, i \in I -> vars i u = vals i) (u \in preim_vars I vals).
proof: Proof. by apply/(iffP bigcapP) => H i /H; rewrite !inE => /eqP. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba