proposition: Lemma div0P : D(P || Q) = 0 <-> P = Q.
proof: Proof. split => [HPQ | ->]; last by rewrite divPP. apply/fdist_ext => a. apply log_id_diff => //; first by move/dominatesP : P_dom_by_Q; exact. apply/esym; move: a (erefl true); apply leR_sumR_eq. - move=> a' _; apply div_diff_ub => //; move/dominatesP : P_dom_by_Q; exact. - transitivity 0; last first. rewrite -{1}oppR0 -{1}HPQ big_morph_oppR. apply eq_bigr => a _; rewrite -mulRN. case/boolP : (P a == 0) => [/eqP ->| H0]; first by rewrite !mul0R. congr (_ * _). have Qa0 := dominatesEN P_dom_by_Q H0. by rewrite -logV ?Rinv_div//; apply divR_gt0; apply /RltP; rewrite -fdist_gt0. rewrite -(big_morph _ (morph_mulRDl _) (mul0R _)) big_split /=. by rewrite -big_morph_oppR !FDist.f1 addR_opp subRR mul0R. Qed.
imports: mathcomp(all_ssreflect ssralg all_algebra reals) Reals mathcomp(Rstruct) ssrR realType_ext Reals_ext ln_facts logb fdist proba