proposition: Lemma f_div_total_pos c : (0 <= f_div_total c)%mcR.
proof: Proof. rewrite ffunE; apply/RleP/mulR_ge0 => //. apply /Rlt_le /invR_gt0 /ltR0n. by rewrite lt0n. 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