proposition: Lemma divPP : D(Q || Q) = 0.
proof: Proof. rewrite /div; apply big1 => a _. case/boolP : (Q a == 0) => [/eqP ->|H0]; first by rewrite mul0R. by rewrite divRR // /log /Log ln_1 div0R mulR0. Qed.
imports: mathcomp(all_ssreflect ssralg all_algebra reals) Reals mathcomp(Rstruct) ssrR realType_ext Reals_ext ln_facts logb fdist proba