proposition: Lemma f_div_total_1 : \sum_(a in A) [ffun a : A => f a / total] a = 1.
proof: Proof. under eq_bigr do rewrite ffunE /=. rewrite /f_div_total -big_distrl -big_morph_natRD. by rewrite sum_f_total /= mulRV // INR_eq0'. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(Rstruct) ssrR realType_ext Reals_ext ssr_ext ssralg_ext logb fdist entropy convex ln_facts jensen num_occ