proposition: Lemma cdiv_ge0 : 0 <= D(V || W | P).
proof: Proof. rewrite cdiv_is_div_joint_dist //; exact/div_ge0/joint_dominates. Qed.
imports: mathcomp(all_ssreflect ssralg finset matrix) Reals mathcomp(Rstruct) ssrR realType_ext Reals_ext ssr_ext ssralg_ext logb ln_facts num_occ fdist entropy channel divergence types jtypes proba jfdist_cond