diff --git a/_CoqProject b/_CoqProject
index 21d6d200..43fa619a 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -11,6 +11,7 @@ lib/Reals_ext.v
 lib/realType_logb.v
 lib/logb.v
 lib/Ranalysis_ext.v
+lib/derive_ext.v
 lib/ssr_ext.v
 lib/f2.v
 lib/ssralg_ext.v
diff --git a/changelog.txt b/changelog.txt
index 6da3a1ad..663ad5a9 100644
--- a/changelog.txt
+++ b/changelog.txt
@@ -3,7 +3,12 @@
 - in ssralg_ext.v
   + lemmas mulr_regl, mulr_regr
 - in realType_ext.v
-  + lemmas x_x2_eq, x_x2_max
+  + lemmas x_x2_eq, x_x2_max, x_x2_pos, x_x2_nneg, expR1_gt2
+- new file derive_ext.v
+  + lemmas differentiable_{ln, Log}
+  + lemmas is_derive{D, B, N, M, V, Z, X, _sum}_eq
+  + lemmas is_derive1_{lnf, lnf_eq, Logf, Logf_eq, LogfM, LogfM_eq, LogfV, LogfV_eq}
+  + lemmas derivable1_mono, derivable1_homo
 
 - lemma `conv_pt_cset_is_convex` changed into a `Let`
 
diff --git a/lib/derive_ext.v b/lib/derive_ext.v
new file mode 100644
index 00000000..02ab3029
--- /dev/null
+++ b/lib/derive_ext.v
@@ -0,0 +1,223 @@
+(* 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 interval.
+From mathcomp Require Import ring lra.
+From mathcomp Require Import mathcomp_extra classical_sets functions.
+From mathcomp Require Import set_interval.
+From mathcomp Require Import reals Rstruct topology normedtype.
+From mathcomp Require Import realfun derive exp.
+Require Import realType_ext realType_logb ssralg_ext.
+
+(******************************************************************************)
+(*        Additional lemmas about differentiation and derivatives             *)
+(*                                                                            *)
+(* Variants of lemmas (mean value theorem, etc.) from mathcomp-analysis       *)
+(*                                                                            *)
+(* TODO: document lemmas                                                      *)
+(*                                                                            *)
+(******************************************************************************)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Import Order.TTheory GRing.Theory Num.Theory.
+Import numFieldTopology.Exports.
+Import numFieldNormedType.Exports.
+
+Local Open Scope ring_scope.
+
+Section differentiable.
+
+Lemma differentiable_ln {R : realType} (x : R) : 0 < x -> differentiable (@ln R) x.
+Proof. move=>?; exact/derivable1_diffP/ex_derive/is_derive1_ln. Qed.
+
+Lemma differentiable_Log {R : realType} (n : nat) (x : R) :
+  0 < x -> (1 < n)%nat -> differentiable (@Log R n) x.
+Proof.
+move=> *.
+apply: differentiableM.
+  exact: differentiable_ln.
+apply: differentiableV=> //.
+rewrite prednK; last exact: (@ltn_trans 1).
+by rewrite neq_lt ln_gt0 ?orbT// ltr1n.
+Qed.
+
+End differentiable.
+
+Section is_derive.
+
+Lemma is_deriveD_eq [R : numFieldType] [V W : normedModType R] [f g : V -> W]
+  [x v : V] [Df Dg D : W] :
+  is_derive x v f Df -> is_derive x v g Dg -> Df + Dg = D ->
+  is_derive x v (f + g) D.
+Proof. by move=> ? ? <-; exact: is_deriveD. Qed.
+
+Lemma is_deriveB_eq [R : numFieldType] [V W : normedModType R] [f g : V -> W]
+  [x v : V] [Df Dg D : W] :
+  is_derive x v f Df -> is_derive x v g Dg -> Df - Dg = D ->
+  is_derive x v (f - g) D.
+Proof. by move=> ? ? <-; exact: is_deriveB. Qed.
+
+Lemma is_deriveN_eq [R : numFieldType] [V W : normedModType R] [f : V -> W]
+  [x v : V] [Df D : W] :
+  is_derive x v f Df -> - Df = D -> is_derive x v (- f) D.
+Proof. by move=> ? <-; exact: is_deriveN. Qed.
+
+Lemma is_deriveM_eq [R : numFieldType] [V : normedModType R] [f g : V -> R]
+  [x v : V] [Df Dg D : R] :
+  is_derive x v f Df -> is_derive x v g Dg ->
+  f x *: Dg + g x *: Df = D ->
+  is_derive x v (f * g) D.
+Proof. by move=> ? ? <-; exact: is_deriveM. Qed.
+
+Lemma is_deriveV_eq [R : realType] [f : R -> R] [x v Df D : R] :
+  f x != 0 ->
+  is_derive x v f Df ->
+  - f x ^- 2 *: Df = D ->
+  is_derive x v (inv_fun f) D.
+Proof. by move=> ? ? <-; exact: is_deriveV. Qed.
+
+Lemma is_deriveZ_eq [R : numFieldType] [V W : normedModType R] [f : V -> W]
+  (k : R) [x v : V] [Df D : W] :
+  is_derive x v f Df -> k *: Df = D ->
+  is_derive x v (k \*: f) D.
+Proof. by move=> ? <-; exact: is_deriveZ. Qed.
+
+Lemma is_deriveX_eq [R : numFieldType] [V : normedModType R] [f : V -> R]
+  (n : nat) [x v : V] [Df D: R] :
+  is_derive x v f Df -> (n.+1%:R * f x ^+ n) *: Df = D ->
+  is_derive x v (f ^+ n.+1) D.
+Proof. by move=> ? <-; exact: is_deriveX. Qed.
+
+Lemma is_derive_sum_eq [R : numFieldType] [V W : normedModType R] [n : nat]
+  [h : 'I_n -> V -> W] [x v : V] [Dh : 'I_n -> W] [D : W] :
+  (forall i : 'I_n, is_derive x v (h i) (Dh i)) ->
+  \sum_(i < n) Dh i = D ->
+  is_derive x v (\sum_(i < n) h i) D.
+Proof. by move=> ? <-; exact: is_derive_sum. Qed.
+
+Lemma is_derive1_lnf [R : realType] [f : R -> R] [x Df : R] :
+  is_derive x 1 f Df -> 0 < f x ->
+  is_derive x 1 (ln (R := R) \o f) (Df / f x).
+Proof.
+move=> hf fx0.
+rewrite mulrC; apply: is_derive1_comp.
+exact: is_derive1_ln.
+Qed.
+
+Lemma is_derive1_lnf_eq [R : realType] [f : R -> R] [x Df D : R] :
+  is_derive x 1 f Df -> 0 < f x ->
+  Df / f x = D ->
+  is_derive x 1 (ln (R := R) \o f) D.
+Proof. by move=> ? ? <-; exact: is_derive1_lnf. Qed.
+
+Lemma is_derive1_Logf [R : realType] [f : R -> R] [n : nat] [x Df : R] :
+  is_derive x 1 f Df -> 0 < f x -> (1 < n)%nat ->
+  is_derive x 1 (Log n (R := R) \o f) ((ln n%:R)^-1 * Df / f x).
+Proof.
+move=> hf fx0 n1.
+rewrite (mulrC _ Df) -mulrA mulrC.
+apply: is_derive1_comp.
+rewrite mulrC; apply: is_deriveM_eq.
+  exact: is_derive1_ln.
+by rewrite scaler0 add0r prednK ?mulr_regr // (@ltn_trans 1).
+Qed.
+
+Lemma is_derive1_Logf_eq [R : realType] [f : R -> R] [n : nat] [x Df D : R] :
+  is_derive x 1 f Df -> 0 < f x -> (1 < n)%nat ->
+  (ln n%:R)^-1 * Df / f x = D ->
+  is_derive x 1 (Log n (R := R) \o f) D.
+Proof. by move=> ? ? ? <-; exact: is_derive1_Logf. Qed.
+
+Lemma is_derive1_LogfM [R : realType] [f g : R -> R] [n : nat] [x Df Dg : R] :
+  is_derive x 1 f Df -> is_derive x 1 g Dg ->
+  0 < f x -> 0 < g x -> (1 < n)%nat ->
+  is_derive x 1 (Log n (R := R) \o (f * g)) ((ln n%:R)^-1 * (Df / f x + Dg / g x)).
+Proof.
+move=> hf hg fx0 gx0 n1.
+apply: is_derive1_Logf_eq=> //.
+  exact: mulr_gt0.
+rewrite -!mulr_regr /(f * g) invfM /= -mulrA; congr (_ * _).
+rewrite addrC (mulrC _^-1) mulrDl; congr (_ + _); rewrite -!mulrA;  congr (_ * _).
+  by rewrite mulrA mulfV ?gt_eqF // div1r.
+by rewrite mulrCA mulfV ?gt_eqF // mulr1.
+Qed.
+
+Lemma is_derive1_LogfM_eq [R : realType] [f g : R -> R] [n : nat] [x Df Dg D : R] :
+  is_derive x 1 f Df -> is_derive x 1 g Dg ->
+  0 < f x -> 0 < g x -> (1 < n)%nat ->
+  (ln n%:R)^-1 * (Df / f x + Dg / g x) = D ->
+  is_derive x 1 (Log n (R := R) \o (f * g)) D.
+Proof. by move=> ? ? ? ? ? <-; exact: is_derive1_LogfM. Qed.
+
+Lemma is_derive1_LogfV [R : realType] [f : R -> R] [n : nat] [x Df : R] :
+  is_derive x 1 f Df -> 0 < f x -> (1 < n)%nat ->
+  is_derive x 1 (Log n (R := R) \o (inv_fun f)) (- (ln n%:R)^-1 * (Df / f x)).
+Proof.  
+move=> hf fx0 n1.
+apply: is_derive1_Logf_eq=> //;
+  [by apply/is_deriveV; rewrite gt_eqF | by rewrite invr_gt0 |].
+rewrite invrK -mulr_regl !(mulNr,mulrN) -mulrA; congr (- (_ * _)).
+by rewrite expr2 invfM mulrC !mulrA mulfV ?gt_eqF // div1r mulrC.
+Qed.
+
+Lemma is_derive1_LogfV_eq [R : realType] [f : R -> R] [n : nat] [x Df D : R] :
+  is_derive x 1 f Df -> 0 < f x -> (1 < n)%nat ->
+  - (ln n%:R)^-1 * (Df / f x) = D ->
+  is_derive x 1 (Log n (R := R) \o (inv_fun f)) D.
+Proof. by move=> ? ? ? <-; exact: is_derive1_LogfV. Qed.
+
+End is_derive.
+
+Section derivable_monotone.
+
+(* generalizing Ranalysis_ext.pderive_increasing_ax_{open_closed,closed_open} *)
+Lemma derivable1_mono [R : realType] (a b : itv_bound R) (f : R -> R) (x y : R) :
+  x \in Interval a b -> y \in Interval a b ->
+  {in Interval a b, forall x, derivable f x 1} ->
+  (forall t : R, forall Ht : t \in `]x, y[, 0 < 'D_1 f t) ->
+  x < y -> f x < f y.
+Proof.
+rewrite !itv_boundlr=> /andP [ax xb] /andP [ay yb].
+move=> derivable_f df_pos xy.
+have HMVT1: ({within `[x, y], continuous f})%classic.
+  apply: derivable_within_continuous=> z /[!itv_boundlr] /andP [xz zy].
+  apply: derivable_f.
+  by rewrite itv_boundlr (le_trans ax xz) (le_trans zy yb).
+have HMVT0: forall z : R, z \in `]x, y[ -> is_derive z 1 f ('D_1 f z).
+  move=> z /[!itv_boundlr] /andP [xz zy].
+  apply/derivableP/derivable_f.
+  rewrite itv_boundlr.
+  rewrite (le_trans (le_trans ax (lexx x : BLeft x <= BRight x)%O) xz).
+  by rewrite (le_trans (le_trans zy (lexx y : BLeft y <= BRight y)%O) yb).
+rewrite -subr_gt0.
+have[z xzy ->]:= MVT xy HMVT0 HMVT1.
+by rewrite mulr_gt0// ?df_pos// subr_gt0.
+Qed.
+
+Lemma derivable1_homo [R : realType] (a b : itv_bound R) (f : R -> R) (x y : R) :
+  x \in Interval a b -> y \in Interval a b ->
+  {in Interval a b, forall x, derivable f x 1} ->
+  (forall t:R, forall Ht : t \in `]x, y[, 0 <= 'D_1 f t) ->
+  x <= y -> f x <= f y.
+Proof.
+rewrite !itv_boundlr=> /andP [ax xb] /andP [ay yb].
+move=> derivable_f df_nneg xy.
+have HMVT1: ({within `[x, y], continuous f})%classic.
+  apply: derivable_within_continuous=> z /[!itv_boundlr] /andP [xz zy].
+  apply: derivable_f.
+  by rewrite itv_boundlr (le_trans ax xz) (le_trans zy yb).
+have HMVT0: forall z : R, z \in `]x, y[ -> is_derive z 1 f ('D_1 f z).
+  move=> z /[!itv_boundlr] /andP [xz zy].
+  apply/derivableP/derivable_f.
+  rewrite itv_boundlr.
+  rewrite (le_trans (le_trans ax (lexx x : BLeft x <= BRight x)%O) xz).
+  by rewrite (le_trans (le_trans zy (lexx y : BLeft y <= BRight y)%O) yb).
+rewrite -subr_ge0.
+move: xy; rewrite le_eqVlt=> /orP [/eqP-> | xy]; first by rewrite subrr.
+have[z xzy ->]:= MVT xy HMVT0 HMVT1.
+by rewrite mulr_ge0// ?df_nneg// subr_ge0 ltW.
+Qed.
+
+End derivable_monotone.
diff --git a/lib/realType_ext.v b/lib/realType_ext.v
index a46bec47..4c2e15e4 100644
--- a/lib/realType_ext.v
+++ b/lib/realType_ext.v
@@ -2,7 +2,7 @@
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum.
-From mathcomp Require Import reals normedtype.
+From mathcomp Require Import reals normedtype sequences.
 From mathcomp Require Import mathcomp_extra boolp.
 From mathcomp Require Import lra ring Rstruct.
 
@@ -108,18 +108,55 @@ Notation "p '.~'" := (onem p).
 
 Section about_the_pow_function.
 Local Open Scope ring_scope.
-Context {R : realFieldType}.
 
-Lemma x_x2_eq (q : R) : q * (1 - q) = 4^-1 - 4^-1 * (2 * q - 1) ^+ 2.
+Lemma x_x2_eq {R : realFieldType} (q : R) : q * (1 - q) = 4^-1 - 4^-1 * (2 * q - 1) ^+ 2.
 Proof. by field. Qed.
 
-Lemma x_x2_max (q : R) : q * (1 - q) <= 4^-1.
+Lemma x_x2_max {R : realFieldType} (q : R) : q * (1 - q) <= 4^-1.
 Proof.
 rewrite x_x2_eq.
 have : forall a b : R, 0 <= b -> a - b <= a. move=>  *; lra.
 apply; apply mulr_ge0; [lra | exact: exprn_even_ge0].
 Qed.
 
+Lemma x_x2_pos {R : realFieldType} (q : R) : 0 < q < 1 -> 0 < q * (1 - q).
+Proof.
+move=> q01.
+rewrite [ltRHS](_ : _ = - (q - 2^-1)^+2 + (2^-2)); last by field.
+rewrite addrC subr_gt0 -exprVn -[ltLHS]real_normK ?num_real//.
+rewrite ltr_pXn2r// ?nnegrE; [| exact: normr_ge0 | lra].
+have/orP[H|H]:= le_total (q - 2^-1) 0.
+  rewrite (ler0_norm H); lra.
+rewrite (ger0_norm H); lra.
+Qed.
+
+Lemma x_x2_nneg {R : realFieldType} (q : R) : 0 <= q <= 1 -> 0 <= q * (1 - q).
+Proof.
+case/andP=> q0 q1.
+have[->|qneq0]:= eqVneq q 0; first lra.
+have[->|qneq1]:= eqVneq q 1; first lra.
+have: 0 < q < 1 by lra.
+by move/x_x2_pos/ltW.
+Qed.
+
+(* TODO: prove expR1_lt3 too; PR to mca *)
+Lemma expR1_gt2 {R : realType} : 2 < expR 1 :> R.
+Proof.
+rewrite /expR /exp_coeff.
+apply: (@lt_le_trans _ _ (series (fun n0 : nat => 1 ^+ n0 / n0`!%:R) 3)).
+  rewrite /series /=.
+  under eq_bigr do rewrite expr1n.
+  rewrite big_mkord.
+  rewrite big_ord_recl /= divr1 ltrD2l.
+  rewrite big_ord_recl /= divr1 -[ltLHS]addr0 ltrD2l.
+  rewrite big_ord_recl big_ord0 addr0 !factS fact0 /bump /= addn0 !muln1.
+  by rewrite mulr_gt0// invr_gt0.
+apply: limr_ge; first exact: is_cvg_series_exp_coeff_pos.
+exists 3=>// n /= n3.
+rewrite -subr_ge0 sub_series_geq// sumr_ge0// => i _.
+by rewrite mulr_ge0// ?invr_ge0// exprn_ge0.
+Qed.
+
 End about_the_pow_function.
 
 
diff --git a/probability/pinsker.v b/probability/pinsker.v
index 46bc6ee3..49bcf8c8 100644
--- a/probability/pinsker.v
+++ b/probability/pinsker.v
@@ -1,11 +1,15 @@
 (* 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.
-Require Import Reals Lra.
-From mathcomp Require Import mathcomp_extra Rstruct reals.
-Require Import ssrR Reals_ext realType_ext Ranalysis_ext ssr_ext.
-Require Import logb ln_facts bigop_ext convex fdist divergence.
-Require Import variation_dist partition_inequality.
+
+From mathcomp Require Import all_ssreflect ssralg ssrnum interval.
+From mathcomp Require Import ring lra.
+From mathcomp Require Import mathcomp_extra classical_sets functions.
+From mathcomp Require Import set_interval.
+From mathcomp Require Import reals Rstruct topology normedtype.
+From mathcomp Require Import realfun sequences derive exp.
+Require Import realType_ext realType_logb ssr_ext ssralg_ext bigop_ext.
+Require Import derive_ext.
+Require Import fdist divergence variation_dist partition_inequality.
 
 (******************************************************************************)
 (*                       Pinsker's Inequality                                 *)
@@ -20,316 +24,310 @@ Unset Strict Implicit.
 Import Prenex Implicits.
 
 Import Order.TTheory GRing.Theory Num.Theory.
+Import numFieldTopology.Exports.
+Import numFieldNormedType.Exports.
 
-Local Open Scope R_scope.
+Local Open Scope ring_scope.
 Local Open Scope fdist_scope.
 
-Definition pinsker_fun p c := fun q =>
-  p * log (div_fct (fun _ => p) id q) +
-  (1 - p) * log (div_fct (fun _ => 1 - p) (fun q => 1 - q) q) -
-  4 * c * comp (fun x => x ^2) (fun q => p - q) q.
+Section pinsker_fun_def.
+Variable R : realType.
+
+Definition pinsker_fun (p c q : R) :=
+  p * log (p / q) +
+  (1 - p) * log ((1 - p) / (1 - q)) -
+  4 * c * (p - q) ^+ 2.
+
+Definition pinsker_fun' (p c : R) := fun q =>
+  (q - p) * ((q * (1 - q) * ln 2)^-1 - 8 * c).
+
+Definition pinsker_function_spec (c q : R) :=
+  - log (1 - q) - 4 * c * q ^+ 2.
+
+Definition pinsker_function_spec' (c q : R) :=
+   ((1 - q) * ln 2)^-1 - 8 * c * q.
 
-Lemma derive_pinsker_fun (p : R) c : 0 < p < 1 ->
-  pderivable (pinsker_fun p c) (fun q => 0 < q < 1).
+Lemma pinsker_fun_p0 c q : q < 1 -> pinsker_fun 0 c q = pinsker_function_spec c q.
 Proof.
-move=> [H0p Hp1] q /= [Hq1 Hq2].
-rewrite /pinsker_fun.
-apply: derivable_pt_minus.
-  apply derivable_pt_plus.
-    apply derivable_pt_mult.
-      exact: derivable_pt_const.
-    apply derivable_pt_comp.
-      apply derivable_pt_mult.
-        apply derivable_pt_const.
-      apply derivable_pt_inv.
-      exact/eqP/gtR_eqF.
-      apply derivable_pt_id.
-    apply derivable_pt_Log.
-    exact: divR_gt0.
-  apply derivable_pt_mult.
-    exact: derivable_pt_const.
-  apply derivable_pt_comp.
-    apply derivable_pt_div.
-      apply derivable_pt_const.
-      apply derivable_pt_Rminus.
-      move=> abs; lra.
-  apply derivable_pt_Log.
-  by apply divR_gt0 => //; lra.
-apply derivable_pt_mult.
-  exact: derivable_pt_const.
-by apply: derivable_pt_comp; [exact: derivable_pt_Rminus|exact: derivable_pt_pow].
-Defined.
-
-Definition pinsker_fun' p c := fun q =>
-  (q - p) * (inv_fct (fun q => (q * (1 - q) * ln 2)) q - 8 * c).
-
-Lemma derive_pt_pinsker_fun p (Hp : 0 < p < 1) c q (Hq : 0 < q < 1)
-  (pr : derivable_pt (pinsker_fun p c) q) :
-  derive_pt (pinsker_fun p c) q pr = pinsker_fun' p c q.
+move=> q1.
+rewrite /pinsker_fun /pinsker_function_spec /=.
+rewrite mul0r subr0 !add0r mul1r sqrrN.
+by rewrite logDiv// ?subr_gt0// log1 add0r.
+Qed.
+
+Lemma pinsker_fun_onem p c q : pinsker_fun (1 - p) c (1 - q) = pinsker_fun p c q.
 Proof.
-transitivity (derive_pt (pinsker_fun p c) q (@derive_pinsker_fun _ c Hp q Hq)).
-  by apply proof_derive_irrelevance.
-rewrite /pinsker_fun /derive_pinsker_fun.
-case: Hp => Hp1 Hp2.
-case: Hq => Hq1 Hq2.
-rewrite !(derive_pt_minus,derive_pt_plus,derive_pt_comp,derive_pt_ln,
-  derive_pt_const,derive_pt_mult,derive_pt_inv,derive_pt_id,derive_pt_div,
-  derive_pt_pow).
-rewrite !(mul0R,mulR0,addR0,add0R,Rminus_0_l) /= (_ : INR 2 = 2) //.
-rewrite /pinsker_fun' /div_fct [X in _ = X]mulRBr.
-f_equal; last by field.
-rewrite (_ : id q = q)// 2!Rinv_div.
-have -> : p * (/ ln 2 * (q / p) * (p * (-1 / q²))) = - (p / q) * / ln 2.
-  rewrite !mulRA /Rsqr.
-  field.
-  split; [exact/eqP/ln2_neq0 | split => ?; lra].
-have -> : (1 - p) * (/ ln 2 * ((1 - q) / (1 - p)) * (- (-1 * (1 - p)) / (1 - q)²)) =
-  (((1 - p) / (1 - q))) * / ln 2.
-  rewrite /Rsqr.
-  field.
-  split; [exact/eqP/ln2_neq0 | split => ?; lra].
-rewrite /inv_fct.
-field.
-by split; [exact/eqP/ln2_neq0 | split => ?; lra].
+rewrite /pinsker_fun [X in X + _ = _]addrC.
+congr (_ + _ - _).
+  by rewrite !opprD !opprK !addrA !subrr !add0r.
+by rewrite -sqrrN !opprD !opprK addrCA !addrA subrr add0r.
 Qed.
 
-Definition pinsker_function_spec c q := - log (1 - q) - 4 * c * q ^ 2.
+Lemma pinsker_fun_p p c : pinsker_fun p c p = 0.
+Proof.
+rewrite /pinsker_fun subrr expr0n /= mulr0 subr0.
+have [->|p0] := eqVneq p 0.
+  by rewrite mul0r !subr0 add0r mul1r div1r invr1 log1.
+have [->|p1] := eqVneq p 1.
+  by rewrite divr1 log1 subrr mul0r mulr0 addr0.
+rewrite divff // divff ?subr_eq0 1?eq_sym//.
+by rewrite log1 !mulr0 addr0.
+Qed.
 
-Definition pinsker_function_spec' c q0 :=
-   / ((1 - q0) * ln 2) - 8 * c * q0.
+End pinsker_fun_def.
 
-Lemma pderivable_pinsker_function_spec c :
-  pderivable (pinsker_function_spec c) (fun q => 0 <= q < 1).
+Section pinsker_function_analysis.
+Variable R : realType.
+
+Lemma derivable_pinsker_fun (p c v : R) : 0 < p < 1 ->
+  {in [pred q | 0 < q < 1], forall q, derivable (pinsker_fun p c) q v}.
 Proof.
-move=> q0 Hq0.
-rewrite /pinsker_function_spec.
-apply derivable_pt_minus.
-  apply derivable_pt_opp.
-  apply derivable_pt_comp.
-    apply derivable_pt_Rminus.
-  apply derivable_pt_Log.
-  rewrite /= in Hq0.
-  decompose [and] Hq0; clear Hq0; lra.
-by apply: derivable_pt_mult; [exact: derivable_pt_const|exact: derivable_pt_pow].
-Defined.
-
-Lemma derive_pt_pinsker_function_spec c q0 (Hq0 : 0 <= q0 < 1)
-  (pr : derivable_pt (pinsker_function_spec c) q0) :
-  derive_pt (pinsker_function_spec c) q0 pr = pinsker_function_spec' c q0.
+move=> /andP [H0p Hp1] /= q /[!inE] /andP [Hq1 Hq2].
+apply: diff_derivable.
+rewrite /pinsker_fun.
+apply: differentiableB; last by [].
+apply: differentiableD.
+  apply: differentiableM; first by [].
+  apply: differentiable_comp.
+    apply: differentiableM; first by [].
+    by apply: differentiableV; rewrite // gt_eqF.
+  apply: differentiable_Log=> //.
+  exact: divr_gt0.
+apply: differentiableM; first by [].
+apply: differentiable_comp.
+  apply: differentiableM=> //.
+  apply: differentiableV=> //.
+  lra.
+apply: differentiable_Log=> //.
+by apply: divr_gt0; lra.
+Qed.
+
+Lemma is_derive1_pinsker_fun
+  (p : R) (Hp : 0 < p < 1) (c q : R) (Hq : 0 < q < 1) :
+  is_derive q 1 (pinsker_fun p c) (pinsker_fun' p c q).
 Proof.
-rewrite (proof_derive_irrelevance _ (pderivable_pinsker_function_spec c Hq0)) //.
+case/andP: Hp => Hp1 Hp2.
+case/andP: Hq => Hq1 Hq2.
+rewrite /pinsker_fun /pinsker_fun'.
+under [F in is_derive _ _ F]boolp.funext=> x.
+  rewrite -sqrrN opprB.
+  rewrite (_ : (x - p) ^+ 2 = ((fun x => x - p) ^+ 2) x); last by [].
+  over.
+rewrite mulrBr; apply: is_deriveB=> /=; last first.
+  apply: is_deriveZ_eq.
+  rewrite expr1 -!mulr_regl.
+  ring.
+rewrite (_ : q - p = p * (- (1 - q)) + (1 - p) * q ); last by ring.
+rewrite mulrDl; apply: is_deriveD=> /=.
+  rewrite -!mulrA; apply: is_deriveZ=> /=.
+  apply: is_derive1_LogfM_eq=> //.
+  - by apply: is_deriveV; rewrite gt_eqF.
+  - by rewrite invr_gt0.
+  - rewrite mulr_algl -mulr_regl; field.
+    by rewrite ln2_neq0 /= subr_eq0 gt_eqF//= !gt_eqF.
+rewrite -!mulrA; apply: is_deriveZ=> /=.
+rewrite invfM mulrA mulfV ?gt_eqF//.
+apply: is_derive1_LogfM_eq=> //=.
+- by apply: is_deriveV; rewrite subr_eq0 gt_eqF.
+- by rewrite subr_gt0.
+- by rewrite invr_gt0 subr_gt0.
+  rewrite -mulr_regl; field.
+  by rewrite ln2_neq0 /= !subr_eq0 !gt_eqF.
+Qed.
+
+Lemma derive1_pinsker_fun (p : R) (Hp : 0 < p < 1) c q (Hq : 0 < q < 1) :
+  'D_1 (pinsker_fun p c) q = pinsker_fun' p c q.
+Proof. by have/@derive_val:= is_derive1_pinsker_fun Hp c Hq. Qed.
+
+Lemma derivable_pinsker_function_spec (c v : R) :
+  {in [pred q | 0 <= q < 1],
+      forall q, derivable (pinsker_function_spec c) q v}.
+Proof.
+move=> q /[!inE] /andP [q0 q1].
+apply: diff_derivable.
 rewrite /pinsker_function_spec.
-rewrite derive_pt_minus.
-rewrite derive_pt_opp.
-rewrite derive_pt_comp.
-rewrite derive_pt_Log.
-rewrite derive_pt_mult.
-rewrite derive_pt_pow.
-rewrite derive_pt_const.
-rewrite mul0R add0R /= /pinsker_function_spec' (_ : INR 2 = 2) //.
-field.
-split; [exact/eqP/ln2_neq0|case: Hq0 => ? ? ?; lra].
-Defined.
-
-Lemma pinsker_fun_increasing_on_0_to_1 (c : R) (Hc : c <= / (2 * ln 2)) :
-  forall x y,
-  0 <= x < 1 -> 0 <= y < 1 -> x <= y ->
-  pinsker_function_spec c x <= pinsker_function_spec c y.
+apply: differentiableB; last by [].
+apply/differentiableN/differentiable_comp; first by [].
+apply: differentiable_Log=> //.
+by rewrite subr_gt0.
+Qed.
+
+Lemma is_derive1_pinsker_function_spec (c q : R) (Hq : 0 <= q < 1) :
+  is_derive q 1 (pinsker_function_spec c) (pinsker_function_spec' c q).
 Proof.
-apply pderive_increasing_closed_open with (pderivable_pinsker_function_spec c).
-lra.
-move=> t Ht.
-rewrite derive_pt_pinsker_function_spec // /pinsker_function_spec'.
-apply (@leR_trans (/ ((1 - t) * ln 2) - 8 * t / (2 * ln 2))); last first.
-  apply leR_add2l.
-  rewrite leR_oppr oppRK -mulRA /Rdiv -[X in _ <= X]mulRA -/(Rdiv _ _).
-  apply leR_wpmul2l; first lra.
-  rewrite mulRC; apply leR_wpmul2l => //.
-  by case: Ht.
-apply (@leR_trans ((2 - 8 * t * (1 - t)) / (2 * (1 - t) * ln 2))); last first.
-  apply Req_le.
-  field.
-  split; [exact/eqP/ln2_neq0 | case: Ht => ? ? ?; lra].
-apply divR_ge0; last first.
-  rewrite mulRC mulRA.
-  apply mulR_gt0.
-    apply mulR_gt0 => //; lra.
-  case: Ht => ? ?; lra.
-have H2 : -2 <= - 8 * t * (1 - t).
-  rewrite !mulNR -mulRA.
-  rewrite leR_oppr oppRK [X in _ <= X](_ : 2 = 8 * / 4); last by field.
-  apply leR_wpmul2l; [lra | exact: x_x2_max].
-move: H2 => /RleP; rewrite -mulRA RmultE mulNr lerNl opprK.
-by move=> /RleP; rewrite -!RmultE mulRA subR_ge0.
+move: Hq=> /andP [q0 q1].
+apply: is_deriveB.
+  apply: is_deriveN_eq; first by apply: is_derive1_Logf=> //; rewrite subr_gt0.
+  by simpl; field; rewrite ln2_neq0 subr_eq0 gt_eqF.
+have->: 8 * c = 4 * c * 2 by ring.
+apply: is_deriveZ_eq.
+by rewrite -!mulr_regr; ring.
 Qed.
 
-Lemma pinsker_function_spec_pos c q :
-  0 <= c <= / (2 * ln 2) ->
-  0 <= q < 1 ->
-  0 <= pinsker_function_spec c q.
+Lemma derive1_pinsker_function_spec (c : R) q (Hq : 0 <= q < 1) :
+  'D_1 (pinsker_function_spec c) q = pinsker_function_spec' c q.
+Proof. by have/@derive_val:= is_derive1_pinsker_function_spec c Hq. Qed.
+
+Lemma pinsker_fun_p0_increasing_on_0_to_1 (c : R) (Hc : c <= (2 * ln 2)^-1) :
+  forall (x y : R),
+  x \in `[0, 1[ -> y \in `[0, 1[ -> x <= y ->
+  pinsker_fun 0 c x <= pinsker_fun 0 c y.
 Proof.
-move=> Hc [q0 q1].
-rewrite (_ : 0 = pinsker_function_spec c 0); last first.
-  by rewrite /pinsker_function_spec /= subR0 /log Log_1; field.
-apply pinsker_fun_increasing_on_0_to_1 => //.
-by case: Hc.
+move=> x y x01 y01.
+have x1: x < 1 by have:= x01; rewrite in_itv /=; lra.
+have y1: y < 1 by have:= y01; rewrite in_itv /=; lra.
+rewrite !pinsker_fun_p0//.
+apply: (derivable1_homo x01 y01).
+  exact: derivable_pinsker_function_spec.
+move=> q xqy.
+move: x01 y01 xqy; rewrite !in_itv /==> x01 y01 xqy.
+rewrite derive1_pinsker_function_spec; last lra.
+rewrite /pinsker_function_spec'.
+rewrite subr_ge0 mulrAC.
+rewrite -ler_pdivlMl ?mulr_gt0//; last lra.
+rewrite (le_trans Hc)//.
+rewrite !invfM mulrA ler_pM2r ?invr_gt0 ?ln2_gt0//.
+rewrite (_ : 8^-1 = 2^-1 * 4^-1); last by field.
+rewrite -[leLHS]mulr1 -!mulrA ler_pM2l; last lra.  
+rewrite -ler_pdivrMr -!invfM; last by rewrite invr_gt0 mulr_gt0; lra.
+by rewrite invrK mul1r x_x2_max.
 Qed.
 
-Section pinsker_function_analysis.
-Variables p q : {prob R}.
+Lemma pinsker_fun_p0_pos (c q : R) :
+  0 <= c <= (2 * ln 2)^-1 ->
+  q \in `[0, 1[ ->
+  0 <= pinsker_fun 0 c q.
+Proof.
+move=> ? /[dup] q01 /[!in_itv] /= q01'.
+rewrite [leLHS](_ : _ = pinsker_fun 0 c 0); last first.
+  by rewrite pinsker_fun_p0 // /pinsker_function_spec /= subr0 log1; field.
+apply pinsker_fun_p0_increasing_on_0_to_1=> //; [lra | | lra].
+by rewrite in_itv /= lexx /=.
+Qed.
 
-Lemma pinsker_fun_p c : pinsker_fun (Prob.p p) c (Prob.p p) = 0.
+Let derivableN_pinsker_fun (p c : R) v (Hp' : 0 < p < 1) :
+  {in [pred q | 0 < q <= p],
+      forall q, derivable (fun x => - pinsker_fun p c x) q v}.
 Proof.
-rewrite /pinsker_fun /= /div_fct /comp subRR mul0R mulR0 subR0.
-have [->|p0] := eqVneq p 0%:pr.
-  by rewrite mul0R !subR0 add0R mul1R div1R invR1 /log Log_1.
-have [->|p1] := eqVneq p 1%:pr.
-  by rewrite divR1 /log Log_1 subRR mul0R mulR0 addR0.
-rewrite divRR; last by rewrite subR_eq0' eq_sym.
-by rewrite /log Log_1 divRR // /log Log_1; field.
+move=> x /[!inE] ?.
+apply/derivableN/derivable_pinsker_fun=> //.
+by rewrite inE; lra.
 Qed.
 
-Lemma pinsker_fun_pderivable1 c (Hp' : 0 < Prob.p p < 1) :
-  pderivable (fun x => - pinsker_fun (Prob.p p) c x) (fun q => 0 < q <= Prob.p p).
-move=> x [Hx1 Hx2].
-apply derivable_pt_opp.
-apply: (@derive_pinsker_fun _ c Hp').
-case: Hp' => Hp'1 Hp'2.
-split => //.
+Lemma pinsker_fun'_ge0 (p c q : R) :
+  c <= (2 * ln 2)^-1 -> 0 < q < 1 -> p <= q -> 0 <= pinsker_fun' p c q.
+Proof.
+move=> Hc q01 pq.
+rewrite /pinsker_fun' mulr_ge0 ?(subr_ge0 p)//.
+rewrite (@le_trans _ _ (4 / ln 2 - 8 * c)) //.
+  rewrite subr_ge0 -ler_pdivlMl//.
+  by rewrite [leRHS](_ : _ = (2 * ln 2)^-1); last by lra.
+rewrite lerB// invfM ler_pM// ?invr_ge0 ?ln2_ge0//.
+rewrite -[leLHS]invrK lef_pV2 ?x_x2_max// posrE ?x_x2_pos//.
 lra.
-Defined.
+Qed.
 
-Lemma pinsker_fun_decreasing_on_0_to_p (c : R) (Hc : c <= / (2 * ln 2))
-  (p01 : 0 < Prob.p p < 1) :
-  forall x y, 0 < x <= Prob.p p -> 0 < y <= Prob.p p -> x <= y ->
-  pinsker_fun (Prob.p p) c y <= pinsker_fun (Prob.p p) c x.
+Lemma pinsker_fun'_le0 (p c q : R) :
+  c <= (2 * ln 2)^-1 -> 0 < q < 1 -> q <= p -> pinsker_fun' p c q <= 0.
 Proof.
-move=> x y Hx Hy xy.
-rewrite -[X in _ <= X]oppRK leR_oppr.
-move: x y Hx Hy xy.
-apply pderive_increasing_open_closed with (pinsker_fun_pderivable1 c p01).
-  by case: p01.
-move=> t [t0 tp].
-rewrite /pinsker_fun_pderivable1.
-rewrite derive_pt_opp.
-rewrite derive_pt_pinsker_fun //; last lra.
-rewrite /pinsker_fun' /div_fct.
-have Hlocal : 0 <= / ln 2 by exact/invR_ge0.
-have X : 0 <= (/ (t * (1 - t) * ln 2) - 8 * c).
-  rewrite subR_ge0; apply (@leR_trans (4 / ln 2)).
-    apply (@leR_trans  (8 * / (2 * ln 2))).
-      apply leR_wpmul2l => //; lra.
-    rewrite invRM; last 2 first.
-      by apply/eqP.
-      exact/ln2_neq0.
-    rewrite mulRA; apply leR_wpmul2r => //; lra.
-  rewrite invRM; last 2 first.
-    by apply/gtR_eqF/mulR_gt0; lra.
-    exact/ln2_neq0.
-  apply leR_wpmul2r => //.
-  rewrite -(invRK 4).
-  apply leR_inv => //.
-    by apply/mulR_gt0 => //; lra.
-  exact: x_x2_max.
-by rewrite /inv_fct -mulNR; apply mulR_ge0 => //; lra.
+move=> Hc q01 qp.
+rewrite /pinsker_fun' -opprB mulNr -oppr_ge0 opprK.
+rewrite mulr_ge0 ?(subr_ge0 q)//.
+rewrite (@le_trans _ _ (4 / ln 2 - 8 * c)) //.
+  rewrite subr_ge0 -ler_pdivlMl//.
+  by rewrite [leRHS](_ : _ = (2 * ln 2)^-1); last by lra.
+rewrite lerB// invfM ler_pM// ?invr_ge0 ?ln2_ge0//.
+rewrite -[leLHS]invrK lef_pV2 ?x_x2_max// posrE ?x_x2_pos//.
+lra.
 Qed.
 
-Lemma pinsker_fun_pderivable2 c (Hp' : 0 < Prob.p p < 1) :
-  pderivable (fun x : R => pinsker_fun (Prob.p p) c x) (fun q : R => Prob.p p <= q < 1).
-move=> x [Hx1 Hx2].
-apply: (@derive_pinsker_fun _ c Hp').
-split => //.
-case: Hp' => Hp'1 Hp'2.
-lra.
-Defined.
+Lemma pinsker_fun_decreasing_on_0_to_p (p c : R) (Hc : c <= (2 * ln 2)^-1)
+  (p01 : 0 < p < 1) (x y : R) :
+  x \in `]0, p] -> y \in `]0, p] -> x <= y ->
+  pinsker_fun p c y <= pinsker_fun p c x.
+Proof.
+move=> /[dup] x0p /[1!in_itv] /= x0p' /[dup] y0p /[!in_itv] /= y0p' xy.
+rewrite -lerN2.
+set f := (fun x => -pinsker_fun p c x).
+apply (derivable1_homo x0p y0p (derivableN_pinsker_fun p01))=> //.
+move=> t /[dup] xty /[!in_itv] /= xty'; have: 0 < t < 1 by lra.
+rewrite deriveN; last first.
+  apply: derivable_pinsker_fun=> //.
+  by rewrite inE; lra.
+move /(is_derive1_pinsker_fun p01 c) /@derive_val ->.
+by rewrite oppr_ge0 pinsker_fun'_le0; lra.
+Qed.
 
-Lemma pinsker_fun_increasing_on_p_to_1 (c : R) (Hc : c <= / (2 * ln 2))
-  (p01 : 0 < Prob.p p < 1) :
-  forall x y, Prob.p p <= x < 1 -> Prob.p p <= y < 1 -> x <= y ->
-  pinsker_fun (Prob.p p) c x <= pinsker_fun (Prob.p p) c y.
+Lemma pinsker_fun_increasing_on_p_to_1 (p c : R) (Hc : c <= (2 * ln 2)^-1)
+  (p01 : 0 < p < 1) :
+  forall x y, x \in `[p, 1[ -> y \in `[p, 1[ -> x <= y ->
+  pinsker_fun p c x <= pinsker_fun p c y.
 Proof.
-apply pderive_increasing_closed_open with (pinsker_fun_pderivable2 c p01).
-  by case: p01.
-move=> t [pt t1].
-rewrite /pinsker_fun_pderivable2.
-rewrite derive_pt_pinsker_fun //; last lra.
-rewrite /pinsker_fun' /div_fct.
-have X : 0 <= (/ (t * (1 - t) * ln 2) - 8 * c).
-  have : forall a b, b <= a -> 0 <= a - b by move=> *; lra.
-  apply.
-  have Hlocal : 0 <= / ln 2 by exact/invR_ge0.
-  have /eqP Hlocal2 : t * (1 - t) <> 0 by apply/eqP/gtR_eqF/mulR_gt0; lra.
-  apply (@leR_trans (4 / ln 2)).
-    apply (@leR_trans (8 * / (2 * ln 2))).
-      apply/RleP.
-      rewrite 2!RmultE ler_pM2l//; last first.
-        by apply/RltP; rewrite (_ : 0%mcR = 0)//; lra.
-      exact/RleP.
-    rewrite invRM ?mulRA; last 2 first.
-      exact/eqP.
-      exact/ln2_neq0.
-    by apply leR_wpmul2r => //; lra.
-  rewrite invRM //; last exact/ln2_neq0.
-  apply leR_wpmul2r => //.
-  rewrite -(invRK 4) //=.
-  apply leR_inv => //.
-    by apply/mulR_gt0; lra.
-  exact: x_x2_max.
-rewrite /inv_fct; apply mulR_ge0 => //; lra.
+move=> x y.
+move=> /[dup] /[1!in_itv] /= ?; rewrite (_ : x = 1 - (1 - x)); [move=>? | ring].
+move=> /[dup] /[1!in_itv] /= ?; rewrite (_ : y = 1 - (1 - y)); [move=>? | ring].
+rewrite (_ : p = 1 - (1 - p)); last ring.
+move=> ?.
+set x' := 1 - x; set y' := 1 - y; set p' := 1 - p.
+rewrite [leLHS]pinsker_fun_onem [leRHS]pinsker_fun_onem.
+apply: (pinsker_fun_decreasing_on_0_to_p Hc); rewrite /x' /y' /p' ?in_itv /=; lra.
 Qed.
 
 End pinsker_function_analysis.
 
+
 Local Open Scope reals_ext_scope.
 
 Section pinsker_fun_pos.
+Variable R : realType.
 Variables p q : {prob R}.
 Variable A : finType.
 Hypothesis card_A : #|A| = 2%nat.
 Hypothesis P_dom_by_Q :
   fdist_binary card_A p (Set2.a card_A) `<< fdist_binary card_A q (Set2.a card_A).
 
-Lemma pinsker_fun_pos c : 0 <= c <= / (2 * ln 2) -> 0 <= pinsker_fun (Prob.p p) c (Prob.p q).
+Lemma pinsker_fun_pos (c : R) : 0 <= c <= (2 * ln 2)^-1 -> 0 <= pinsker_fun p c q.
 Proof.
 move=> Hc.
 set a := Set2.a card_A. set b := Set2.b card_A.
 have [p0|p0] := eqVneq p 0%:pr.
   subst p.
-  rewrite /pinsker_fun /div_fct /comp.
-  rewrite !(mul0R,mulR0,addR0,add0R,Rminus_0_l,subR0).
+  rewrite /pinsker_fun.
+  rewrite !(mul0r,mulr0,addr0,add0r,sub0r,subr0).
   have [q1|q1] := eqVneq q 1%:pr.
     subst q.
     exfalso.
     move/dominatesP : P_dom_by_Q => /(_ a).
-    by rewrite !fdist_binaryE !/onem subrr eqxx subr0 -R1E -R0E; lra.
-  apply: leR_trans.
-    apply: (@pinsker_function_spec_pos _ (Prob.p q) Hc); split=> //.
-    by apply/RltP; rewrite -prob_lt1.
-  rewrite /pinsker_function_spec.
-  apply: Req_le.
-  by rewrite mul1R div1R /log LogV; [field|
-    rewrite subR_gt0; apply /RltP; rewrite -prob_lt1].
+    by rewrite !fdist_binaryE !/onem subrr eqxx subr0; lra.
+  apply: le_trans.
+    apply: (@pinsker_fun_p0_pos _ _ q Hc).
+    rewrite in_itv /=; apply/andP; split=> //.
+    by rewrite -prob_lt1.
+  rewrite pinsker_fun_p0 /pinsker_function_spec -?prob_lt1//.
+  rewrite le_eqVlt; apply/orP; left; apply/eqP.
+  by rewrite mul1r div1r logV; [field | rewrite subr_gt0 -prob_lt1].
 have [p1|p1] := eqVneq p 1%:pr.
   subst p.
-  rewrite /pinsker_fun /div_fct /comp subRR mul0R addR0.
+  rewrite /pinsker_fun subrr mul0r addr0.
   have [q0|q0] := eqVneq q 0%:pr.
     subst q.
     exfalso.
     move/dominatesP : P_dom_by_Q => /(_ b).
     rewrite !fdist_binaryE /onem subrr eq_sym (negbTE (Set2.a_neq_b card_A)) /=.
     by move=> /(_ erefl)/eqP; rewrite oner_eq0.
-  apply: leR_trans.
-    have : 0 <= 1 - Prob.p q < 1.
-      split; first by rewrite subR_ge0.
-      by rewrite ltR_subl_addr -{1}(addR0 1) ltR_add2l; apply/RltP/ prob_gt0.
-    exact: pinsker_function_spec_pos Hc.
-  rewrite /pinsker_function_spec.
-  apply Req_le.
-  rewrite mul1R div1R /log LogV; [|by apply/RltP/prob_gt0].
-  rewrite /id (_ : 1 - (1 - Prob.p q) = Prob.p q) //; by field.
+  apply: le_trans.
+    have : 0 <= 1 - q < 1.
+      apply/andP; split; first by rewrite subr_ge0.
+      by rewrite ltrBlDr -{1}(addr0 1) ltrD2l; apply/prob_gt0.
+    exact: pinsker_fun_p0_pos Hc.
+  rewrite pinsker_fun_p0 /pinsker_function_spec; last first.
+    by rewrite -[ltRHS]subr0 ltrD2l ltrN2 -prob_gt0.
+  rewrite le_eqVlt; apply/orP; left; apply/eqP.
+  rewrite mul1r div1r logV; [|by apply/prob_gt0].
+  by rewrite (_ : 1 - (1 - q) = q :> R) //=; by field.
 have [q0|q0] := eqVneq q 0%:pr.
   subst q.
-  rewrite /pinsker_fun /div_fct /comp.
+  rewrite /pinsker_fun.
   exfalso.
   move/dominatesP : P_dom_by_Q => /(_ b).
   rewrite !fdist_binaryE eq_sym (negbTE (Set2.a_neq_b card_A)) => /(_ erefl) p0_.
@@ -338,22 +336,20 @@ have [q1|q1] := eqVneq q 1%:pr.
   subst q.
   exfalso.
   move/dominatesP : P_dom_by_Q => /(_ a).
-  rewrite !fdist_binaryE /onem subrr eqxx subR_eq0 => /(_ erefl) p1_.
+  rewrite !fdist_binaryE /onem subrr eqxx=> /(_ erefl) /eqP /[!subr_eq0] /eqP p1_.
   by move/eqP : p1; apply; apply/val_inj; rewrite /= -p1_.
 rewrite -(pinsker_fun_p p c).
-case: (Rlt_le_dec (Prob.p q) (Prob.p p)) => qp.
+have/orP[qp|qp]:= le_total q p.
   apply pinsker_fun_decreasing_on_0_to_p => //.
   - lra.
-  - by split; apply/RltP; [rewrite -prob_gt0 | rewrite -prob_lt1].
-  - by split; [apply/RltP/prob_gt0 | exact/ltRW].
-  - split; [by apply/RltP/prob_gt0 | ].
-    by apply/RleP; rewrite lexx.
-  - exact/ltRW.
+  - by apply/andP; split; [rewrite -prob_gt0 | rewrite -prob_lt1].
+  - by apply/andP; split; [apply/prob_gt0 | ].
+  - by apply/andP; split; [exact/prob_gt0 | exact/lexx].
 apply pinsker_fun_increasing_on_p_to_1 => //.
 - lra.
-- by split; apply/RltP; [rewrite -prob_gt0 |rewrite -prob_lt1].
-- by split; [by apply/RleP; rewrite lexx |apply/RltP/prob_lt1].
-- by split => //; apply/RltP; rewrite -prob_lt1.
+- by apply/andP; split; [rewrite -prob_gt0 |rewrite -prob_lt1].
+- by apply/andP; split; [by rewrite lexx |apply/prob_lt1].
+- by apply/andP; split => //; rewrite -prob_lt1.
 Qed.
 
 End pinsker_fun_pos.
@@ -362,6 +358,7 @@ Local Open Scope divergence_scope.
 Local Open Scope variation_distance_scope.
 
 Section Pinsker_2_bdist.
+Variable R : realType.
 Variables p q : {prob R}.
 Variable A : finType.
 Hypothesis card_A : #|A| = 2%nat.
@@ -371,78 +368,61 @@ Let Q := fdist_binary card_A q (Set2.a card_A).
 
 Hypothesis P_dom_by_Q : P `<< Q.
 
-Lemma pinsker_fun_p_eq c : pinsker_fun (Prob.p p) c (Prob.p q) = D(P || Q) - c * d(P , Q) ^ 2.
+Lemma pinsker_fun_p_eq c : pinsker_fun p c q = D(P || Q) - c * d(P , Q) ^+ 2.
 Proof.
 pose a := Set2.a card_A. pose b := Set2.b card_A.
 set pi := P a.
 set pj := P b.
 set qi := Q a.
 set qj := Q b.
-have Hpi : pi = 1 - Prob.p p by rewrite /pi /P fdist_binaryxx.
-have Hqi : qi = 1 - Prob.p q by rewrite /qi /= fdist_binaryxx.
-have Hpj : pj = Prob.p p.
+have Hpi : pi = 1 - p by rewrite /pi /P fdist_binaryxx.
+have Hqi : qi = 1 - q by rewrite /qi /= fdist_binaryxx.
+have Hpj : pj = p.
   by rewrite /pj /= fdist_binaryE eq_sym (negbTE (Set2.a_neq_b card_A)).
-have Hqj : qj = Prob.p q.
+have Hqj : qj = q.
   by rewrite /qj /= fdist_binaryE eq_sym (negbTE (Set2.a_neq_b card_A)).
-transitivity (D(P || Q) - c * (`| Prob.p p - Prob.p q | + `| (1 - Prob.p p) - (1 - Prob.p q) |) ^ 2).
+transitivity (D(P || Q) - c * (`| (p : R) - q | + `| (1 - p) - (1 - q) |) ^+ 2).
   rewrite /pinsker_fun /div Set2sumE -/a -/b -/pi -/pj -/qi -/qj Hpi Hpj Hqi Hqj.
-  set tmp := (`| _ | + _) ^ 2.
-  have -> : tmp = 4 * (Prob.p p - Prob.p q) ^ 2.
-    rewrite /tmp (_ : 1 - Prob.p p - (1 - Prob.p q) = Prob.p q - Prob.p p); last by field.
-    rewrite sqrRD (distRC (Prob.p q) (Prob.p p)) -mulRA -{3}(pow_1 `| Prob.p p - Prob.p q |).
-    rewrite -expRS sqR_norm; ring.
-  rewrite [X in _ = _ + _ - X]mulRA.
-  rewrite [in X in _ = _ + _ - X](mulRC c).
+  set tmp := (`| _ | + _) ^+ 2.
+  have -> : tmp = 4 * ((p : R) - q) ^+ 2.
+    rewrite /tmp (_ : 1 - p - (1 - q) = (q : R) - p); last by simpl; ring.
+    rewrite sqrrD (distrC (q : R) (p : R)) -{3}(expr1 `|(p : R) - q|).
+    by rewrite -exprS real_normK ?num_real//; ring.
+  rewrite [X in _ = _ + _ - X]mulrA.
+  rewrite [in X in _ = _ + _ - X](mulrC c).
   congr (_ - _).
-  case/boolP : (p == 0%:pr) => [/eqP |] p0.
-    rewrite p0 !mul0R subR0 addR0 add0R !mul1R /log (*_Log_1*) /Rdiv.
-    have [q1|q1] := eqVneq q 1%:pr.
-      move/dominatesP : P_dom_by_Q => /(_ (Set2.a card_A)).
-      rewrite -/pi -/qi Hqi q1 subRR => /(_ erefl).
-      by rewrite Hpi p0 subR0 -R0E => ?; exfalso; lra.
-    rewrite /log LogM; last 2 first.
-      lra.
-      by apply/invR_gt0; rewrite subR_gt0; apply/RltP/prob_lt1.
-      rewrite LogV; last by apply/subR_gt0/RltP/prob_lt1.
-      by rewrite Log_1.
+  case/boolP : (p == 0%:pr) => [/eqP |] p0;
+    first by rewrite p0 !mul0r subr0 addr0 add0r !mul1r.
   have [q0|q0] := eqVneq q 0%:pr.
     move/dominatesP : P_dom_by_Q => /(_ (Set2.b card_A)).
     rewrite -/pj -/qj Hqj q0 => /(_ erefl).
     rewrite Hpj => abs.
-    have : p == 0%:pr by apply/eqP/val_inj.
+    have : p == 0%:pr by exact/eqP/val_inj.
     by rewrite (negbTE p0).
-  rewrite /div_fct /comp /= (_ : id (Prob.p q) = Prob.p q) //.
   have [->|p1] := eqVneq p 1%:pr.
-    rewrite subRR !mul0R /Rdiv /log LogM //; last first.
-      apply/invR_gt0; by apply/RltP/prob_gt0.
-      rewrite Log_1 /= mul1R LogV //; last by apply/RltP/prob_gt0.
-      by rewrite !(add0R,mul1R,addR0,sub0R).
-  rewrite /log LogM //; last 2 first.
-    by apply/RltP/prob_gt0.
-    by apply/invR_gt0/RltP/prob_gt0.
-  rewrite LogV //; last by apply/RltP/prob_gt0.
+    rewrite subrr !mul0r logM //; last first.
+      by rewrite invr_gt0; exact/prob_gt0.
+    by rewrite !(add0r,mul1r,addr0,sub0r).
+  rewrite logM //; [| exact/prob_gt0 | by rewrite invr_gt0; exact/prob_gt0].
+  rewrite logV //; last exact/prob_gt0.
   have [q1|q1] := eqVneq q 1%:pr.
     move/dominatesP : P_dom_by_Q => /(_ (Set2.a card_A)).
-    rewrite -/pi -/qi Hqi q1 subRR => /(_ erefl).
-    rewrite Hpi subR_eq0 => abs.
-    have : p == 1%:pr by apply/eqP/val_inj.
-    by rewrite (negbTE p1).
-  rewrite /Rdiv LogM ?subR_gt0 //; last 2 first.
-    by apply/RltP/prob_lt1.
-    by apply/invR_gt0; rewrite subR_gt0; apply/RltP/prob_lt1.
-  rewrite LogV; last by rewrite subR_gt0; apply/RltP/prob_lt1.
-  ring.
+    rewrite -/pi -/qi Hqi q1 subrr => /(_ erefl).
+    by rewrite Hpi=> ->; rewrite mul0r addr0 add0r.
+  rewrite logM ?invr_gt0 ?subr_gt0 -?prob_lt1//.
+  rewrite logV ?subr_gt0-?prob_lt1//.
+  by rewrite addrC.
 congr (_ - _ * _).
-by rewrite /var_dist Set2sumE // -/pi -/pj -/qi -/qj Hpi Hpj Hqi Hqj addRC.
+by rewrite /var_dist Set2sumE // -/pi -/pj -/qi -/qj Hpi Hpj Hqi Hqj addrC.
 Qed.
 
-Lemma Pinsker_2_inequality_bdist : / (2 * ln 2) * d(P , Q) ^ 2 <= D(P || Q).
+Lemma Pinsker_2_inequality_bdist : (2 * ln 2)^-1 * d(P , Q) ^+ 2 <= D(P || Q).
 Proof.
 set lhs := _ * _.
 set rhs := D(_ || _).
-rewrite -subR_ge0 -pinsker_fun_p_eq.
+rewrite -subr_ge0 -pinsker_fun_p_eq.
 apply pinsker_fun_pos with A card_A => //.
-by split; [exact/invR_ge0/mulR_gt0 | by apply/RleP; rewrite lexx].
+by rewrite lexx andbT invr_ge0 mulr_ge0// ln2_ge0.
 Qed.
 
 End Pinsker_2_bdist.
@@ -452,7 +432,7 @@ Variables (A : finType) (P Q : {fdist A}).
 Hypothesis card_A : #|A| = 2%nat.
 Hypothesis P_dom_by_Q : P `<< Q.
 
-Lemma Pinsker_2_inequality : / (2 * ln 2) * d(P , Q) ^ 2 <= D(P || Q).
+Lemma Pinsker_2_inequality : (2 * ln 2)^-1 * d(P , Q) ^+ 2 <= D(P || Q).
 Proof.
 move: (charac_bdist P card_A) => [r1 Hp].
 move: (charac_bdist Q card_A) => [r2 Hq].
@@ -473,87 +453,76 @@ Local Notation "1" := (true).
 Lemma bipart_dominates :
   let A_ := fun b => if b then [set a | (P a < Q a)%mcR]
                           else [set a | (Q a <= P a)%mcR] in
-  forall (cov : A_ 0 :|: A_ 1 = [set: A]) (dis : A_ 0 :&: A_ 1 = set0),
+  forall (cov : A_ 0 :|: A_ 1 = [set: A]) (dis : A_ 0 :&: A_ 1 = finset.set0),
   bipart dis cov P `<< bipart dis cov Q.
 Proof.
 move=> A_ cov dis; apply/dominatesP => /= b.
 rewrite !ffunE => /psumr_eq0P H.
-transitivity (\sum_(a | a \in A_ b) 0%R).
-  apply eq_bigr => // a ?.
-  by rewrite (dominatesE P_dom_by_Q) // H // => a' ?; exact/pos_ff_ge0.
-by rewrite big_const iter_addR mulR0.
+by apply: big1=> ? ?; rewrite (dominatesE P_dom_by_Q) // ?H //.
 Qed.
 
-Lemma Pinsker_inequality : / (2 * ln 2) * d(P , Q) ^ 2 <= D(P || Q).
+Lemma Pinsker_inequality : (2 * ln 2)^-1 * d(P , Q) ^+ 2 <= D(P || Q).
 Proof.
 pose A0 := [set a | (Q a <= P a)%mcR].
 pose A1 := [set a | (P a < Q a)%mcR].
 pose A_ := fun b => match b with 0 => A0 | 1 => A1 end.
-have cov : A_ 0 :|: A_ 1 = setT.
+have cov : A_ 0 :|: A_ 1 = finset.setT.
   rewrite /= /A0 /A1.
   have -> : [set x | (P x < Q x)%mcR] = ~: [set x | (Q x <= P x)%mcR].
-    by apply/setP => a; rewrite in_set in_setC in_set ltNge.
-  by rewrite setUCr.
-have dis : A_ 0 :&: A_ 1 = set0.
+    by apply/setP => a; rewrite finset.in_set finset.in_setC finset.in_set ltNge.
+  by rewrite finset.setUCr.
+have dis : A_ 0 :&: A_ 1 = finset.set0.
   rewrite /A_ /A0 /A1.
   have -> : [set x | (P x < Q x)%mcR] = ~: [set x | (Q x <= P x)%mcR].
-    by apply/setP => a; rewrite in_set in_setC in_set ltNge.
-  by rewrite setICr.
+    by apply/setP => a; rewrite finset.in_set finset.in_setC finset.in_set ltNge.
+  by rewrite finset.setICr.
 pose P_A := bipart dis cov P.
 pose Q_A := bipart dis cov Q.
 have step1 : D(P_A || Q_A) <= D(P || Q).
   by apply partition_inequality; exact P_dom_by_Q.
-suff : / (2 * ln 2) * d(P , Q) ^2 <= D(P_A || Q_A).
-  move=> ?; apply (@leR_trans (D(P_A || Q_A))) => //; exact/Rge_le.
+suff : (2 * ln 2)^-1 * d(P , Q) ^+ 2 <= D(P_A || Q_A).
+  move=> ?; apply (@le_trans _ _ (D(P_A || Q_A))) => //; exact/ge_le.
 have -> : d( P , Q ) = d( P_A , Q_A ).
   rewrite /var_dist.
   transitivity (\sum_(a | a \in A0) `| P a - Q a | + \sum_(a | a \in A1) `| P a - Q a |).
-    rewrite -big_union //; last by rewrite -setI_eq0 -dis /A_ setIC.
-    apply eq_bigl => a; by rewrite cov in_set.
+    rewrite -big_union //; last by rewrite -setI_eq0 -dis /A_ finset.setIC.
+    apply eq_bigl => a; by rewrite cov finset.in_set.
   transitivity (`| P_A 0 - Q_A 0 | + `| P_A 1 - Q_A 1 |).
     congr (_ + _).
     - rewrite /P_A /Q_A /bipart /= /bipart_pmf /=.
       transitivity (\sum_(a | a \in A0) (P a - Q a)).
-        apply: eq_bigr => a; rewrite /A0 in_set => /RleP Ha.
-        by rewrite geR0_norm ?subR_ge0.
-      rewrite big_split /= geR0_norm; last first.
-        rewrite subR_ge0; rewrite !ffunE.
-        by apply leR_sumR => ?; rewrite inE => /RleP.
-      by rewrite -big_morph_oppR // 2!ffunE addR_opp.
+        apply: eq_bigr => a; rewrite /A0 finset.in_set => Ha.
+        by rewrite ger0_norm ?subr_ge0.
+      rewrite big_split /= ger0_norm; last first.
+        rewrite subr_ge0; rewrite !ffunE.
+        by apply ler_sum => ?; rewrite inE.
+      by rewrite -big_morph_oppr // 2!ffunE.
     - rewrite /P_A /Q_A /bipart /= !ffunE /=.
       have [A1_card | A1_card] : #|A1| = O \/ (0 < #|A1|)%nat.
         destruct (#|A1|); [tauto | by right].
       + move/eqP : A1_card; rewrite cards_eq0; move/eqP => A1_card.
-        by rewrite A1_card !big_set0 subRR normR0.
+        by rewrite A1_card !big_set0 subrr normr0.
       + transitivity (\sum_(a | a \in A1) - (P a - Q a)).
-          apply eq_bigr => a; rewrite /A1 in_set => Ha.
-          by rewrite ltR0_norm // subR_lt0; exact/RltP.
-        rewrite -big_morph_oppR // big_split /= ltR0_norm; last first.
-          rewrite subR_lt0; apply ltR_sumR_support => // a.
-          by rewrite /A1 in_set => /RltP.
-        by rewrite -big_morph_oppR.
+          apply eq_bigr => a; rewrite /A1 finset.in_set => Ha.
+          by rewrite ltr0_norm // subr_lt0.
+        rewrite -big_morph_oppr // big_split /= ltr0_norm; last first.
+          rewrite subr_lt0; apply: ltR_sumR_support => // a.
+          by rewrite /A1 finset.in_set.
+        by rewrite -big_morph_oppr.
   by rewrite big_bool /= /bipart_pmf !ffunE /=.
 exact/(Pinsker_2_inequality card_bool)/bipart_dominates.
 Qed.
 
-Lemma Pinsker_inequality_weak : d(P , Q) <= sqrt (2 * D(P || Q)).
+Lemma Pinsker_inequality_weak : d(P , Q) <= Num.sqrt (2 * D(P || Q)).
 Proof.
-rewrite -(sqrt_Rsqr (d(P , Q))); last first.
-  exact/RleP/pos_var_dist.
-apply sqrt_le_1_alt.
-apply (@leR_pmul2l (/ 2)); first by apply invR_gt0; lra.
-apply (@leR_trans (D(P || Q))); last first.
-  rewrite mulRA mulVR // ?mul1R; [| exact/gtR_eqF].
-  by apply/RleP; rewrite lexx.
-apply: (leR_trans _ Pinsker_inequality).
-rewrite (_ : forall x, Rsqr x = x ^ 2); last first.
-  by move=> ?; rewrite /Rsqr /pow mulR1.
-apply leR_wpmul2r; first exact: pow_even_ge0.
-apply leR_inv => //; first exact/mulR_gt0.
-rewrite -[X in _ <= X]mulR1.
-apply leR_wpmul2l; first lra.
-rewrite [X in _ <= X](_ : 1%R = ln (exp 1)); last by rewrite ln_exp.
-by apply ln_increasing_le; [lra | exact leR2e].
+rewrite -[leLHS]ger0_norm ?pos_var_dist// -sqrtr_sqr.
+rewrite ler_wsqrtr// -ler_pdivrMl//.
+apply: (le_trans _ Pinsker_inequality).
+rewrite invfM mulrAC ler_peMr//.
+  by rewrite mulr_ge0// ?invr_ge0// sqr_ge0.
+rewrite invf_ge1// ?ln2_gt0//.
+rewrite -[leRHS]expRK.
+by rewrite ler_ln ?posrE// ?expR_gt0// ltW// expR1_gt2.
 Qed.
 
 End Pinsker.