fact: Definition nth_fin_img (i : Tfin_img) : S := tnth (in_tuple (fin_img f)) i.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba