proposition: Lemma f0 x y : (0 <= f x y).
proof: Proof. rewrite ffunE; apply/RleP; exact: prodR_ge0. Qed.
imports: mathcomp(all_ssreflect all_algebra) Reals mathcomp(Rstruct) ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy jfdist_cond