proposition: Lemma fin_imgP y : reflect (exists x : T, y = f x) (y \in fin_img f).
proof: Proof. rewrite mem_undup; apply/(iffP mapP) => -[x]. - move=> _ ->. by exists x. - move=> ->. by exists x; rewrite // mem_enum. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba