proposition: Lemma rev_fin_imgK i : map_fin_img (rev_fin_img i) = i.
proof: Proof. case: i => i isz; apply val_inj => /=. by rewrite f_iinv nthK // undup_uniq. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba