proposition: Lemma f_inj : injective [ffun a : A => nth [::] C (enum_rank a)].
proof: Proof. move=> x y. rewrite !ffunE => /eqP xy. rewrite -(enum_rankK x) -(enum_rankK y); congr enum_val. apply/ord_inj/eqP. rewrite -(@nth_uniq _ [::] C (enum_rank x) (enum_rank y)) //; last first. rewrite /C /ACode /= /acode map_inj_uniq //. exact/enum_uniq. exact/injective_sigma. rewrite /C /ACode /= /acode size_map size_enum_ord prednK //. exact: (fdist_card_neq0 P). rewrite /C /ACode /= /acode size_map size_enum_ord prednK //. exact: (fdist_card_neq0 P). Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(Rstruct) ssrZ ssrR logb Reals_ext realType_ext ssr_ext fdist entropy kraft