fact: Definition kraft_condR (T : finType) (sizes : seq nat) := let n := size sizes in (\sum_(i < n) #|T|%:R^-(nth O sizes i) <= (1 : R))%R.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(Rstruct) ssrZ ssrR logb Reals_ext realType_ext ssr_ext fdist entropy kraft