proposition: Lemma f1 : (\sum_(b in B) f b = 1)%R.
proof: Proof. under eq_bigr do rewrite ffunE /=. rewrite -big_distrl /= -big_morph_natRD exchange_big /=. by move/eqP : (JType.sum_f V) => ->; rewrite mulRV // INR_eq0'. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum fingroup perm) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext logb fdist entropy num_occ channel types