proposition: Lemma f0 (b : B) : (0 <= f b)%mcR.
proof: Proof. rewrite ffunE; apply/RleP/ divR_ge0; [exact/leR0n | exact/ltR0n]. 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