proposition: Lemma nth_fin_imgK x : nth_fin_img (map_fin_img x) = f x.
proof: Proof. rewrite /nth_fin_img /index_fin_img => /=. by rewrite (tnth_nth (f x)) nth_index // mem_undup map_f // 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