proposition: Lemma map_fin_imgK x : f (rev_fin_img (map_fin_img x)) = f x.
proof: Proof. by rewrite /rev_fin_img f_iinv nth_fin_imgK. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba