diff --git a/information_theory/entropy.v b/information_theory/entropy.v
index 78c6bfab..685229b1 100644
--- a/information_theory/entropy.v
+++ b/information_theory/entropy.v
@@ -4,7 +4,7 @@ From mathcomp Require Import all_ssreflect all_algebra fingroup perm.
 Require Import Reals.
 From mathcomp Require Import Rstruct reals.
 Require Import ssrR Reals_ext realType_ext ssr_ext ssralg_ext bigop_ext.
-Require Import logb ln_facts fdist jfdist_cond proba binary_entropy_function.
+Require Import realType_logb (*ln_facts*) fdist jfdist_cond proba binary_entropy_function.
 Require Import divergence.
 
 (******************************************************************************)
@@ -61,10 +61,14 @@ Local Open Scope vec_ext_scope.
 
 Import Order.POrderTheory GRing.Theory Num.Theory.
 
+(* TODO: kludge *)
+Hint Extern 0 ((0 <= _)%coqR) => solve [exact/RleP/FDist.ge0] : core.
+Hint Extern 0 ((_ <= 1)%coqR) => solve [exact/RleP/FDist.le1] : core.
+
 Section entropy_definition.
 Variables (A : finType) (P : {fdist A}).
 
-Definition entropy := - \sum_(a in A) P a * log (P a).
+Definition entropy := - \sum_(a in A) P a * realType_logb.log (P a).
 Local Notation "'`H'" := (entropy).
 
 Lemma entropy_ge0 : 0 <= `H.
@@ -73,8 +77,8 @@ rewrite /entropy big_morph_oppR; apply/RleP/sumr_ge0 => i _; apply/RleP.
 have [->|Hi] := eqVneq (P i) 0; first by rewrite mul0R oppR0.
   (* NB: this step in a standard textbook would be handled as a consequence of lim x->0 x log x = 0 *)
 rewrite mulRC -mulNR; apply mulR_ge0 => //; apply: oppR_ge0.
-rewrite -log1; apply: Log_increasing_le => //.
-by apply/RltP; rewrite lt0r Hi/=.
+rewrite coqRE -(@log1 R); apply/RleP; rewrite ler_log// ?posrE//.
+by rewrite lt0r Hi/=.
 Qed.
 
 End entropy_definition.
@@ -93,13 +97,14 @@ rewrite /entropy /log_RV /= big_morph_oppR.
 by apply eq_bigr => a _; rewrite mulRC -mulNR.
 Qed.
 
-Lemma xlnx_entropy (P : {fdist A}) : `H P = / ln 2 * - \sum_(a : A) xlnx (P a).
+Lemma xlnx_entropy (P : {fdist A}) : `H P = / exp.ln 2 * - \sum_(a : A) xlnx (P a).
 Proof.
 rewrite /entropy mulRN; congr (- _); rewrite big_distrr/=.
-apply: eq_bigr => a _; rewrite /log /Rdiv mulRA mulRC; congr (_ * _).
-rewrite /xlnx; case : ifP => // /RltP Hcase.
-have -> : P a = 0 by case (Rle_lt_or_eq_dec 0 (P a)).
-by rewrite mul0R.
+apply: eq_bigr => a _; rewrite /xlnx /log /Log/=.
+have := FDist.ge0 P a.
+rewrite le_eqVlt => /predU1P[<-|Pa0].
+  by rewrite mul0r if_same mulR0 mul0R.
+by rewrite Pa0 mulRA mulRC !coqRE.
 Qed.
 
 Lemma entropy_uniform n (An1 : #|A| = n.+1) :
@@ -109,8 +114,7 @@ rewrite /entropy.
 under eq_bigr do rewrite fdist_uniformE.
 rewrite big_const iter_addR mulRA RmultE -RinvE.
 rewrite INRE mulRV; last by rewrite An1 -INRE INR_eq0'.
-rewrite -RmultE mul1R logV ?oppRK//; rewrite An1.
-by rewrite -INRE; apply/ltR0n.
+by rewrite -RmultE mul1R !coqRE logV ?An1 ?ltr0n// opprK.
 Qed.
 
 Lemma entropy_H2 (card_A : #|A| = 2%nat) (p : {prob R}) :
diff --git a/lib/binary_entropy_function.v b/lib/binary_entropy_function.v
index 1f170fd2..17430093 100644
--- a/lib/binary_entropy_function.v
+++ b/lib/binary_entropy_function.v
@@ -1,8 +1,9 @@
 (* infotheo: information theory and error-correcting codes in Coq               *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later              *)
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import reals.
 Require Import Reals Lra.
-Require Import ssrR Reals_ext Ranalysis_ext logb.
+Require Import ssrR Reals_ext Ranalysis_ext realType_logb.
 
 (******************************************************************************)
 (*                    The natural entropy function                            *)
@@ -23,7 +24,7 @@ Import Prenex Implicits.
 
 Local Open Scope R_scope.
 
-Definition H2ln := fun p => - p * ln p - (1 - p) * ln (1 - p).
+Definition H2ln {R : realType} : R -> R := fun p : R => (- p * exp.ln p - (1 - p) * exp.ln (1 - p))%mcR.
 
 Lemma derivable_pt_ln_Rminus x : x < 1 -> derivable_pt ln (1 - x).
 Proof.
@@ -33,6 +34,7 @@ apply derivable_pt_lim_ln, subR_gt0.
 assumption.
 Defined.
 
+(*
 Lemma pderivable_H2ln : pderivable H2ln (fun x => 0 < x <= 1/2).
 Proof.
 move=> x /= [Hx0 Hx1].
@@ -122,10 +124,11 @@ case: (Rlt_le_dec q (1/2)) => [H1|].
     lra.
   by apply decreasing_on_half_to_1 => //; lra.
 Qed.
+*)
 
-Definition H2 p := - (p * log p) + - ((1 - p) * log (1 - p)).
+Definition H2 {R : realType} (p : R) : R := (- (p * log p) + - ((1 - p) * log (1 - p)))%mcR.
 
-Lemma bin_ent_0eq0 : H2 0 = 0.
+(*Lemma bin_ent_0eq0 : H2 0 = 0.
 Proof.
 rewrite /H2 /log.
 by rewrite !(Log_1, mulR0, mul0R, oppR0, mul1R, mulR1, add0R, addR0, subR0).
@@ -154,3 +157,4 @@ case: x_0 => [?|<-]; last by rewrite bin_ent_0eq0.
 case: x_1 => [?|->]; last by rewrite bin_ent_1eq0.
 exact: H2_max.
 Qed.
+*)
diff --git a/lib/realType_logb.v b/lib/realType_logb.v
index 20d9d825..b78396b0 100644
--- a/lib/realType_logb.v
+++ b/lib/realType_logb.v
@@ -1,7 +1,7 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum.
-From mathcomp Require Import reals exp.
+From mathcomp Require Import reals exp sequences.
 Require Import realType_ext.
 
 (******************************************************************************)
@@ -21,6 +21,100 @@ Local Open Scope ring_scope.
 
 Import Order.POrderTheory GRing.Theory Num.Theory.
 
-Definition Log {R : realType} (n : R) x := ln x / ln n.
+Section ln_ext.
+Context {R : realType}.
+Implicit Type x : R.
+
+Lemma ln2_gt0 : 0 < ln 2 :> R.
+Proof. by rewrite ln_gt0// ltr1n. Qed.
+
+Lemma ln2_neq0 : ln 2 != 0 :> R. Proof. by rewrite gt_eqF// ln2_gt0. Qed.
+
+Lemma ln_id_cmp x : 0 < x -> ln x <= x - 1.
+Proof.
+move=> x0.
+Admitted.
+
+Lemma ln_id_eq x : 0 < x -> ln x = x - 1 -> x = 1 :> R.
+Proof.
+Admitted.
+
+End ln_ext.
+
+Section xlnx.
+Context {R : realType}.
+
+Definition xlnx (x : R) : R := if (0 < x)%mcR then x * ln x else 0.
+
+Lemma xlnx_0 : xlnx 0 = 0.
+Proof. by rewrite /xlnx mul0r ltxx. Qed.
+
+Lemma xlnx_1 : xlnx 1 = 0.
+Proof. by rewrite /xlnx ltr01 mul1r ln1. Qed.
+
+End xlnx.
+
+
+Section Log.
+Context {R : realType}.
+
+Definition Log (n : nat) x : R := ln x / ln n.-1.+1%:R.
+
+Lemma Log1 (n : nat) : Log n 1 = 0 :> R.
+Proof. by rewrite /Log ln1 mul0r. Qed.
+
+Lemma ler_Log (n : nat) : (1 < n)%N  -> {in Num.pos &, {mono Log n : x y / x <= y :> R}}.
+Proof.
+move=> n1 x y x0 y0.
+rewrite /Log ler_pdivrMr prednK ?(leq_trans _ n1)// ?ln_gt0 ?ltr1n//.
+by rewrite -mulrA mulVf ?mulr1 ?gt_eqF ?ln_gt0 ?ltr1n// ler_ln.
+Qed.
+
+Lemma LogV n x : 0 < x -> Log n x^-1 = - Log n x.
+Proof. by move=> x0; rewrite /Log lnV ?posrE// mulNr. Qed.
+
+Lemma LogM n x y : 0 < x -> 0 < y -> Log n (x * y) = Log n x + Log n y.
+Proof. by move=> *; rewrite /Log -mulrDl lnM. Qed.
+
+Lemma LogDiv n x y : 0 < x -> 0 < y -> Log n (x / y) = Log n x - Log n y.
+Proof. by move=> x0 y0; rewrite LogM ?invr_gt0// LogV. Qed.
+
+End Log.
+
+
+Section log.
+Context {R : realType}.
+Implicit Types x y : R.
 
 Definition log {R : realType} (x : R) := Log 2 x.
+
+Lemma log1 : log 1 = 0 :> R. Proof. by rewrite /log Log1. Qed.
+
+Lemma ler_log : {in Num.pos &, {mono log : x y / x <= y :> R}}.
+Proof. by move=> x y x0 y0; rewrite /log ler_Log. Qed.
+
+Lemma logV x : 0 < x -> log x^-1 = - log x :> R.
+Proof. by move=> x0; rewrite /log LogV. Qed.
+
+Lemma logDiv x y : 0 < x -> 0 < y -> log (x / y) = log x - log y.
+Proof. by move=> x0 y0; exact: (@LogDiv _ _ _ _ x0 y0). Qed.
+
+(* TODO: rename, lemma for Log *)
+Lemma logexp1E : log (expR 1) = (ln 2)^-1 :> R.
+Proof. by rewrite /log /Log/= expRK div1r. Qed.
+
+Lemma log_exp1_Rle_0 : 0 <= log (expR 1) :> R.
+Proof.
+rewrite logexp1E.
+rewrite invr_ge0// ltW//.
+by rewrite ln2_gt0//.
+Qed.
+
+Lemma log_id_cmp x : 0 < x -> log x <= (x - 1) * log (expR 1).
+Proof.
+move=> x0; rewrite logexp1E ler_wpM2r// ?invr_ge0//= ?(ltW (@ln2_gt0 _))//.
+exact/ln_id_cmp.
+Qed.
+
+
+End log.
diff --git a/probability/divergence.v b/probability/divergence.v
index 77505e16..2b69fb69 100644
--- a/probability/divergence.v
+++ b/probability/divergence.v
@@ -1,9 +1,8 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
-From mathcomp Require Import all_ssreflect ssralg all_algebra reals.
-Require Import Reals.
-From mathcomp Require Import Rstruct.
-Require Import ssrR realType_ext Reals_ext ln_facts logb fdist proba.
+From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import Rstruct reals sequences exp.
+Require Import realType_ext realType_logb (*ln_facts logb*) fdist proba.
 
 (******************************************************************************)
 (*    Divergence (or the Kullback-Leibler distance or relative entropy)       *)
@@ -25,38 +24,52 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Import Prenex Implicits.
 
-Local Open Scope R_scope.
+Local Open Scope ring_scope.
 Local Open Scope fdist_scope.
 
+Import Order.POrderTheory GRing.Theory Num.Theory.
+
 (* TODO: rename, move? *)
 Section log_facts.
+Context {R : realType}.
 
 Lemma div_diff_ub x y : 0 <= x -> (y = 0 -> x = 0) -> 0 <= y ->
-                        x * (log (y / x)) <= (y - x) * log (exp 1).
+                        x * (log (y / x)) <= (y - x) * log (expR 1) :> R.
 Proof.
-move=> x0 yx /leR_eqVlt[/esym|] y0.
-- by move: (yx y0) => ->; rewrite y0 subRR 2!mul0R.
-- case/leR_eqVlt : x0 => [/esym ->|x0].
-  + rewrite mul0R subR0; apply mulR_ge0; [exact: ltRW | exact: log_exp1_Rle_0].
+move=> x0 yx; rewrite le_eqVlt => /predU1P[/esym|] y0.
+- by rewrite y0 yx// subrr 2!mul0r.
+- move: x0; rewrite le_eqVlt => /predU1P[/esym ->|x0].
+  + rewrite mul0r subr0 mulr_ge0//; [exact: ltW | ].
+    by rewrite log_exp1_Rle_0.
   + rewrite (_ : y - x = x * (y / x - 1)); last first.
-      by rewrite mulRDr mulRCA mulRV ?mulR1 ?mulRN1 //; exact/gtR_eqF.
-    rewrite -mulRA; apply (leR_wpmul2l (ltRW x0)).
-    by apply/log_id_cmp/mulR_gt0 => //; exact/invR_gt0.
+      by rewrite mulrDr mulrCA mulfV ?gt_eqF// mulr1 mulrN1.
+    rewrite -mulrA; apply (ler_wpM2l (ltW x0)).
+    by rewrite log_id_cmp// divr_gt0.
+Qed.
+
+Lemma log_id_eq x : 0 < x -> log x = (x - 1) * log (expR 1) -> x = 1 :> R.
+Proof.
+move=> Hx'; rewrite logexp1E.
+move=> /(congr1 (fun x => x * ln 2)).
+rewrite -!mulrA mulVf// ?gt_eqF ?ln2_gt0//.
+by rewrite !mulr1; exact: ln_id_eq.
 Qed.
 
 Lemma log_id_diff x y : 0 <= x -> (y = 0 -> x = 0) -> 0 <= y ->
-  x * (log (y / x)) = (y - x) * log (exp 1) -> x = y.
+  x * (log (y / x)) = (y - x) * log (expR 1) -> x = y :> R.
 Proof.
-move=> Hx Hxy /leR_eqVlt[/esym|] y0 Hxy2; first by rewrite y0 Hxy.
-case/leR_eqVlt : Hx => [/esym|] x0.
-- move/esym : Hxy2; rewrite x0 mul0R subR0 mulR_eq0 => -[] //.
-  by rewrite logexp1E => /invR_eq0/eqP; rewrite (negbTE ln2_neq0).
-- apply/esym; rewrite -(@eqR_mul2l (/ x)) //; last exact/nesym/eqP/ltR_eqF/invR_gt0.
-  rewrite mulVR //; last exact/gtR_eqF.
-  apply log_id_eq; first by apply mulR_gt0 => //; exact: invR_gt0.
-  rewrite -(@eqR_mul2l x); last exact/eqP/gtR_eqF.
-  rewrite {1}(mulRC _ y) Hxy2 mulRA mulRBr; congr (_ * _).
-  field; exact/eqP/gtR_eqF.
+move=> Hx Hxy; rewrite le_eqVlt => /predU1P[/esym|] y0 Hxy2; first by rewrite y0 Hxy.
+move: Hx; rewrite le_eqVlt => /predU1P[/esym|] x0.
+- move/esym : Hxy2; rewrite x0 mul0r subr0 => /eqP.
+  rewrite mulf_eq0 => /predU1P[//|/eqP].
+  rewrite logexp1E => /eqP.
+  by rewrite gt_eqF// invr_gt0// ln2_gt0.
+- apply/esym/divr1_eq.
+  apply: log_id_eq; first by rewrite divr_gt0.
+  move: Hxy2.
+  move/(congr1 (fun z => x^-1 * z)).
+  rewrite mulrA mulVf ?gt_eqF// mul1r => ->.
+  by rewrite mulrA mulrBr mulVf ?gt_eqF// (mulrC _ y).
 Qed.
 
 End log_facts.
@@ -69,6 +82,18 @@ Definition div := \sum_(a in A) P a * log (P a / Q a).
 
 End divergence_def.
 
+(* TODO: rename, move *)
+Lemma leR_sumR_eq {R : realType} (A : finType) (f g : A -> R) (P : pred A) :
+   (forall a, P a -> f a <= g a) ->
+   \sum_(a | P a) g a = \sum_(a | P a) f a ->
+   (forall a, P a -> g a = f a).
+Proof.
+move=> H1 H2 i Hi; apply/eqP; rewrite -subr_eq0; apply/eqP.
+move: i Hi; apply: psumr_eq0P.
+  by move=> i Pi; rewrite Num.Theory.subr_ge0 H1.
+by rewrite big_split/= sumrN; apply/eqP; rewrite subr_eq0 H2.
+Qed.
+
 Notation "'D(' P '||' Q ')' " := (div P Q) : divergence_scope.
 
 Local Open Scope divergence_scope.
@@ -76,7 +101,7 @@ Local Open Scope reals_ext_scope.
 Local Open Scope fdist_scope.
 
 Section divergence_prop.
-
+Context {R : realType}.
 Variables (A : finType) (P Q : {fdist A}).
 Hypothesis P_dom_by_Q : P `<< Q.
 
@@ -84,51 +109,44 @@ Lemma div_ge0 : 0 <= D(P || Q).
 Proof.
 rewrite /div [X in _ <= X](_ : _ =
     - \sum_(a | a \in A) P a * (log (Q a / P a))); last first.
-  rewrite big_morph_oppR; apply eq_bigr => a _; rewrite -mulRN.
-  case/boolP : (P a == 0) => [/eqP ->|H0]; first by rewrite !mul0R.
+  rewrite -sumrN; 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 leR_oppr oppR0.
-apply (@leR_trans ((\sum_(a | a \in A) (Q a - P a)) * log (exp 1))).
-  rewrite (big_morph _ (morph_mulRDl _) (mul0R _)).
-  apply leR_sumR => a _; apply: div_diff_ub => //.
-  - exact/RleP/FDist.ge0.
+  by rewrite -logV ?invf_div// divr_gt0//; apply/fdist_gt0.
+rewrite ler_oppr oppr0.
+apply (@le_trans _ _ ((\sum_(a | a \in A) (Q a - P a)) * log (expR 1))).
+  rewrite big_distrl/=.
+  apply: ler_sum => a _; apply: div_diff_ub => //.
   - by move/dominatesP : P_dom_by_Q; exact.
-  - exact/RleP/FDist.ge0.
-rewrite -{1}(mul0R (log (exp 1))); apply (leR_wpmul2r log_exp1_Rle_0).
-by rewrite big_split /= -big_morph_oppR !FDist.f1 addR_opp subRR.
+rewrite -[leRHS](mul0r (log (expR 1))) ler_wpM2r// ?log_exp1_Rle_0//.
+by rewrite big_split /= sumrN !FDist.f1 subrr.
 Qed.
 
 Lemma divPP : D(Q || Q) = 0.
 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.
+case/boolP : (Q a == 0) => [/eqP ->|H0]; first by rewrite mul0r.
+by rewrite divff // log1 mulr0.
 Qed.
 
 Lemma div0P : D(P || Q) = 0 <-> P = Q.
 Proof.
 split => [HPQ | ->]; last by rewrite divPP.
 apply/fdist_ext => a.
-apply log_id_diff.
-- exact/RleP/FDist.ge0.
+apply log_id_diff => //.
 - by move/dominatesP : P_dom_by_Q; exact.
-- exact/RleP/FDist.ge0.
 - apply/esym; move: a (erefl true); apply leR_sumR_eq.
   + move=> a' _; apply div_diff_ub => //.
-    * exact/RleP/FDist.ge0.
     * by move/dominatesP : P_dom_by_Q; exact.
-    * exact/RleP/FDist.ge0.
-  + 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.
+  + apply: (@trans_eq _ _ 0%R); last first.
+      rewrite -{1}oppr0 -{1}HPQ -sumrN.
+      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.
+      by rewrite -logV ?invf_div// divr_gt0// -fdist_gt0.
+    by rewrite -big_distrl/= big_split/= sumrN !FDist.f1 subrr mul0r.
 Qed.
 
 End divergence_prop.
diff --git a/probability/fdist.v b/probability/fdist.v
index db80c4f1..0986f5ef 100644
--- a/probability/fdist.v
+++ b/probability/fdist.v
@@ -139,8 +139,8 @@ Coercion FDist.f : fdist >-> finfun_of.
 HB.instance Definition _ R A := [isSub for @FDist.f R A].
 HB.instance Definition _ R A := [Choice of fdist R A by <:].
 
-#[global] Hint Extern 0 (is_true (0 <= _)%R) => solve [exact: FDist.ge0] : core.
-#[global] Hint Extern 0 (is_true (_ <= 1)%R) => solve [exact: FDist.le1] : core.
+#[global] Hint Extern 0 (is_true (0 <= _)%mcR) => solve [exact: FDist.ge0] : core.
+#[global] Hint Extern 0 (is_true (_ <= 1)%mcR) => solve [exact: FDist.le1] : core.
 
 Notation "R '.-fdist' T" := (fdist R T%type) : fdist_scope.
 Notation "{ 'fdist' T }" := (fdist Rdefinitions.R T%type) : fdist_scope.