diff --git a/information_theory/shannon_fano.v b/information_theory/shannon_fano.v
index 008c88d9..6ab00bdf 100644
--- a/information_theory/shannon_fano.v
+++ b/information_theory/shannon_fano.v
@@ -74,10 +74,10 @@ apply ler_sum => i _.
 rewrite H.
 have Pi0 : 0 < P i by rewrite lt0r Pr0/=.
 apply (@le_trans _ _ (Exp #|T|%:R (- Log #|T|%:R (P i)^-1))); last first.
-  by rewrite LogV// opprK LogK // card_ord natn.
+  by rewrite LogV// opprK natn LogK// card_ord.
 rewrite pow_Exp; last by rewrite card_ord.
-rewrite Exp_oppr lef_pV2// ?posrE ?Exp_gt0//.
-rewrite !card_ord natn Exp_le_increasing//.
+rewrite Exp_oppr card_ord lef_pV2// ?posrE ?Exp_gt0//.
+rewrite Exp_le_increasing// ?ltr1n//.
 rewrite (le_trans (mathcomp_extra.ceil_ge _))//.
 by rewrite natr_absz// ler_int ler_norm.
 Qed.
diff --git a/information_theory/typ_seq.v b/information_theory/typ_seq.v
index baeb8bdb..bb02bbc3 100644
--- a/information_theory/typ_seq.v
+++ b/information_theory/typ_seq.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 ssrnum matrix.
-Require Import Reals Lra.
-From mathcomp Require Import Rstruct.
-Require Import ssrR Reals_ext realType_ext logb.
+From mathcomp Require Import Rstruct reals lra exp.
+Require Import ssr_ext realType_ext realType_logb.
 Require Import fdist proba entropy aep.
 
 (******************************************************************************)
@@ -35,19 +34,19 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Import Prenex Implicits.
 
-Local Open Scope R_scope.
 Local Open Scope fdist_scope.
 Local Open Scope proba_scope.
 Local Open Scope entropy_scope.
+Local Open Scope ring_scope.
 
 Import Order.TTheory GRing.Theory Num.Theory.
 
 Section typical_sequence_definition.
 
-Variables (A : finType) (P : {fdist A}) (n : nat) (epsilon : R).
+Variables (A : finType) (P : {fdist A}) (n : nat) (epsilon : Rdefinitions.R).
 
 Definition typ_seq (t : 'rV[A]_n) :=
-  (exp2 (- n%:R * (`H P + epsilon)) <= P `^ n t <= exp2 (- n%:R * (`H P - epsilon)))%mcR.
+  (2 `^ (- n%:R * (`H P + epsilon)) <= (P `^ n)%fdist t <= 2 `^ (- n%:R * (`H P - epsilon)))%R.
 
 Definition set_typ_seq := [set ta | typ_seq ta].
 
@@ -57,107 +56,112 @@ Notation "'`TS'" := (set_typ_seq) : typ_seq_scope.
 
 Local Open Scope typ_seq_scope.
 
-Lemma set_typ_seq_incl (A : finType) (P : {fdist A}) n epsilon : 0 <= epsilon -> forall r, 1 <= r ->
+Lemma set_typ_seq_incl (A : finType) (P : {fdist A}) n epsilon : 0 <= epsilon ->
   `TS P n (epsilon / 3) \subset `TS P n epsilon.
 Proof.
-move=> e0 r r1.
+move=> e0.
 apply/subsetP => /= x.
-rewrite !inE /typ_seq => /andP[/RleP H2 /RleP H3] [:Htmp].
-apply/andP; split; apply/RleP.
-- apply/(leR_trans _ H2)/Exp_le_increasing => //.
-  rewrite !mulNR leR_oppr oppRK; apply leR_wpmul2l; first exact/leR0n.
-  apply/leR_add2l.
+rewrite !inE /typ_seq => /andP[H2 H3] [:Htmp].
+apply/andP; split.
+- apply/(le_trans _ H2).
+  rewrite ler_powR ?ler1n// !mulNr lerNr opprK; apply ler_wpM2l => //.
+  rewrite lerD2l//.
   abstract: Htmp.
-  rewrite leR_pdivr_mulr; [apply leR_pmulr => //|]; lra.
-- apply/(leR_trans H3)/Exp_le_increasing => //.
-  rewrite !mulNR leR_oppr oppRK; apply leR_wpmul2l; first exact/leR0n.
-  apply leR_add2l; rewrite leR_oppr oppRK; exact Htmp.
+  by rewrite ler_pdivr_mulr// ler_peMr//; lra.
+- apply/(le_trans H3); rewrite ler_powR// ?ler1n//.
+  rewrite !mulNr lerNr opprK; apply ler_wpM2l => //.
+  by rewrite lerD2l lerNr opprK; exact Htmp.
 Qed.
 
 Section typ_seq_prop.
 
-Variables (A : finType) (P : {fdist A}) (epsilon : R) (n : nat).
+Variables (A : finType) (P : {fdist A}) (epsilon : Rdefinitions.R) (n : nat).
 
-Lemma TS_sup : #| `TS P n epsilon |%:R <= exp2 (n%:R * (`H P + epsilon)).
+Lemma TS_sup : #| `TS P n epsilon |%:R <= 2 `^ (n%:R * (`H P + epsilon)).
 Proof.
-suff Htmp : #| `TS P n epsilon |%:R * exp2 (- n%:R * (`H P + epsilon)) <= 1.
-  by rewrite -(mulR1 (exp2 _)) mulRC -leR_pdivr_mulr // /Rdiv -exp2_Ropp -mulNR.
-rewrite (_ : 1 = 1%mcR)// -(FDist.f1 (P `^ n)).
-rewrite (_ : _ * _ = \sum_(x in `TS P n epsilon) (exp2 (- n%:R * (`H P + epsilon)))); last first.
-  by rewrite big_const iter_addR.
-by apply/leR_sumRl => //= i; rewrite inE; case/andP => /RleP.
+suff Htmp : #| `TS P n epsilon |%:R * 2 `^ (- n%:R * (`H P + epsilon)) <= 1.
+  by rewrite -(mulr1 (2 `^ _)) mulrC -ler_pdivrMr // ?powR_gt0// -powRN// -mulNr.
+rewrite -[leRHS](FDist.f1 (P `^ n)%fdist).
+rewrite (_ : _ * _ = \sum_(x in `TS P n epsilon) (2 `^ (- n%:R * (`H P + epsilon)))); last first.
+  by rewrite big_const iter_addr addr0 mulr_natl.
+by apply: leR_sumRl => //= i; rewrite inE; case/andP.
 Qed.
 
 Lemma typ_seq_definition_equiv x : x \in `TS P n epsilon ->
-  exp2 (- n%:R * (`H P + epsilon)) <= P `^ n x <= exp2 (- n%:R * (`H P - epsilon)).
-Proof. by rewrite inE /typ_seq => /andP[? ?]; split; apply/RleP. Qed.
+  2 `^ (- n%:R * (`H P + epsilon)) <= (P `^ n)%fdist x <= 2 `^ (- n%:R * (`H P - epsilon)).
+Proof. by rewrite inE /typ_seq => /andP[? ?]; apply/andP; split. Qed.
 
 Lemma typ_seq_definition_equiv2 x : x \in `TS P n.+1 epsilon ->
-  `H P - epsilon <= - (1 / n.+1%:R) * log (P `^ n.+1 x) <= `H P + epsilon.
+  `H P - epsilon <= - n.+1%:R^-1 * log ((P `^ n.+1)%fdist x) <= `H P + epsilon.
 Proof.
 rewrite inE /typ_seq.
-case/andP => H1 H2; split;
-  apply/RleP; rewrite -(@ler_pM2r _ n.+1%:R) ?ltr0n//.
-- rewrite div1R -[in leRHS]RmultE mulRAC mulNR INRE mulVR; last first.
-    by rewrite mulrn_eq0/= oner_eq0.
-  rewrite mulN1R; apply/RleP.
-  rewrite leR_oppr.
-  apply/(@Exp_le_inv 2) => //.
-  rewrite LogK //; last by apply/(ltR_leR_trans (exp2_gt0 _)); apply/RleP: H1.
-  rewrite mulrC -mulNR -INRE.
-  exact/RleP.
-- rewrite div1R -[in leLHS]RmultE mulRAC mulNR INRE mulVR; last first.
-    by rewrite mulrn_eq0/= oner_eq0.
-  rewrite mulN1R; apply/RleP.
-  rewrite leR_oppl.
-  apply/(@Exp_le_inv 2) => //.
-  rewrite LogK //; last by apply/(ltR_leR_trans (exp2_gt0 _)); apply/RleP: H1.
-  rewrite mulrC -mulNR -INRE.
-  exact/RleP.
+case/andP => H1 H2; apply/andP; split;
+  rewrite -(@ler_pM2r _ n.+1%:R) ?ltr0n//.
+- rewrite mulrAC mulNr mulVf; last by rewrite pnatr_eq0.
+  rewrite mulN1r.
+  rewrite lerNr.
+  rewrite -ler_log ?posrE// in H2; last 2 first.
+    by rewrite (lt_le_trans _ H1)// Exp_gt0//.
+    by rewrite Exp_gt0.
+  by rewrite mulNr powRN logV ?Exp_gt0// log_powR log2 mulr1 mulrC in H2.
+- rewrite mulrAC mulNr mulVf; last by rewrite pnatr_eq0.
+  have := FDist.ge0 ((P `^ n.+1)%fdist) x; rewrite le_eqVlt => /predU1P[H3|H3].
+    have : 0 < 2 `^ (1 *- n.+1 * (`H P + epsilon)).
+      by rewrite Exp_gt0//.
+    rewrite -H3 in H1.
+    by rewrite ltNge H1.
+  rewrite mulN1r.
+  rewrite lerNl.
+  rewrite -ler_log ?posrE// in H1; last first.
+    by rewrite Exp_gt0.
+  by rewrite mulNr powRN logV ?Exp_gt0// log_powR log2 mulr1 mulrC in H1.
 Qed.
 
 End typ_seq_prop.
 
 Section typ_seq_more_prop.
-
-Variables (A : finType) (P : {fdist A}) (epsilon : R) (n : nat).
+Variables (A : finType) (P : {fdist A}) (epsilon : Rdefinitions.R) (n : nat).
 
 Hypothesis He : 0 < epsilon.
 
 Lemma Pr_TS_1 : aep_bound P epsilon <= n.+1%:R ->
-  1 - epsilon <= Pr (P `^ n.+1) (`TS P n.+1 epsilon).
+  1 - epsilon <= Pr (P `^ n.+1)%fdist (`TS P n.+1 epsilon).
 Proof.
 move=> k0_k.
-have -> : Pr P `^ n.+1 (`TS P n.+1 epsilon) =
-  Pr P `^ n.+1 [set i | (i \in `TS P n.+1 epsilon) && (0 < P `^ n.+1 i)%mcR].
+have -> : Pr (P `^ n.+1)%fdist (`TS P n.+1 epsilon) =
+  Pr (P `^ n.+1)%fdist [set i | (i \in `TS P n.+1 epsilon) && (0 < (P `^ n.+1)%fdist i)%mcR].
   congr Pr; apply/setP => /= t; rewrite !inE.
   apply/idP/andP => [H|]; [split => // | by case].
-  case/andP : H => /RleP H _; exact/RltP/(ltR_leR_trans (exp2_gt0 _) H).
+  case/andP : H => H _; apply/(lt_le_trans _ H).
+  by rewrite Exp_gt0//.
 set p := [set _ | _].
-rewrite Pr_to_cplt leR_add2l leR_oppl oppRK.
-have -> : Pr P `^ n.+1 (~: p) =
-  Pr P `^ n.+1 [set x | P `^ n.+1 x == 0] +
-  Pr P `^ n.+1 [set x | (0 < P `^ n.+1 x)%mcR &&
-                (`| - (1 / n.+1%:R) * log (P `^ n.+1 x) - `H P | > epsilon)%mcR].
+rewrite Pr_to_cplt lerD2l lerNl opprK.
+have -> : Pr (P `^ n.+1)%fdist (~: p) =
+  Pr (P `^ n.+1)%fdist [set x | (P `^ n.+1)%fdist x == 0] +
+  Pr (P `^ n.+1)%fdist [set x | (0 < (P `^ n.+1)%fdist x)%mcR &&
+                (`| - n.+1%:R^-1 * log ((P `^ n.+1)%fdist x) - `H P | > epsilon)%mcR].
   have -> : ~: p =
-    [set x | P `^ n.+1 x == 0 ] :|:
-    [set x | (0 < P `^ n.+1 x)%mcR &&
-             (`| - (1 / n.+1%:R) * log (P `^ n.+1 x) - `H P | > epsilon)%mcR].
+    [set x | (P `^ n.+1)%fdist x == 0 ] :|:
+    [set x | (0 < (P `^ n.+1)%fdist x)%mcR &&
+             (`| - n.+1%:R^-1 * log ((P `^ n.+1)%fdist x) - `H P | > epsilon)%mcR].
     apply/setP => /= i; rewrite !inE negb_and orbC.
-    apply/idP/idP => [/orP[/RltP|]|].
-    - move/RltP => H.
-      have {}H : P `^ n.+1 i = 0.
+    apply/idP/idP => [/orP[H|]|].
+    - have {}H : (P `^ n.+1)%fdist i = 0.
         apply/eqP.
         apply/negPn.
         apply: contra H.
-        by have [+ _] := fdist_gt0 (P `^ n.+1) i.
+        by have [+ _] := fdist_gt0 (P `^ n.+1)%fdist i.
       by rewrite H eqxx.
     - rewrite /typ_seq negb_and => /orP[|] LHS.
-      + have [//|H1] := eqVneq (P `^ n.+1 i) 0.
-        have {}H1 : 0 < P `^ n.+1 i by apply/RltP; rewrite lt0r H1/=.
-        apply/andP; split; first exact/RltP.
-        move/RleP: LHS => /ltRNge/(@Log_increasing 2 _ _ Rlt_1_2 H1).
-        rewrite /exp2 ExpK // mulRC mulRN -mulNR -ltR_pdivr_mulr; last exact/ltR0n.
+      + have [//|H1] := eqVneq ((P `^ n.+1)%fdist i) 0.
+        have {}H1 : 0 < (P `^ n.+1)%fdist i by rewrite lt0r H1/=.
+        rewrite /= H1/=.
+        move: LHS; rewrite -ltNge => /log_increasing => /(_ H1).
+        rewrite log_powR mulNr log2 mulr1.
+ mulN1r. mulrC. mulrN -mulNr -ltr_pdivr_mulr.
+ 
+
+; last exact/ltR0n.
         rewrite /Rdiv mulRC ltR_oppr => /RltP; rewrite -ltrBrDl => LHS.
         rewrite div1r// mulNr -RinvE ger0_norm// -INRE//.
         by move/RltP : LHS; move/(ltR_trans He)/ltRW/RleP.
diff --git a/lib/logb.v b/lib/logb.v
index 88c73537..c04cd978 100644
--- a/lib/logb.v
+++ b/lib/logb.v
@@ -414,3 +414,4 @@ rewrite big_cons LogM//; last first.
   by apply/RltP/prodr_gt0 => a _; exact/RltP.
 by rewrite [RHS]big_cons oppRD; congr (_ + _)%coqR.
 Qed.
+
diff --git a/lib/realType_logb.v b/lib/realType_logb.v
index 957d583a..ff9539ef 100644
--- a/lib/realType_logb.v
+++ b/lib/realType_logb.v
@@ -115,38 +115,46 @@ End Log.
 Section Exp.
 Context {R : realType}.
 
-Definition Exp (n : nat) (x : R) := expR (x * ln n%:R).
+(* TODO: rm *)
+Definition Exp (n : R) (x : R) := n `^ x.
 
-Lemma pow_Exp (x : nat) n : (0 < x)%N -> x%:R ^+ n = Exp x n%:R.
-Proof. by move=> x0; rewrite /Exp expRM_natl lnK// posrE ltr0n. Qed.
+Lemma pow_Exp (x : R) n : (0 <= x) -> x ^+ n = Exp x n%:R.
+Proof. by move=> x0; rewrite /Exp powR_mulrn. Qed.
 
-Lemma LogK n x : (1 < n)%N -> 0 < x -> Exp n (Log n x) = x.
+Lemma LogK n x : (1 < n)%N -> 0 < x -> Exp n%:R (Log n x) = x.
 Proof.
 move=> n1 x0.
-rewrite /Log /Exp prednK// 1?ltnW// -mulrA mulVf// ?mulr1 ?lnK//.
-by rewrite gt_eqF// -ln1 ltr_ln// ?posrE// ?ltr1n// ltr0n ltnW.
+rewrite /Exp /Log prednK// 1?ltnW//.
+rewrite powRrM {1}/powR ifF; last first.
+  by apply/negbTE; rewrite powR_eq0 negb_and pnatr_eq0 gt_eqF// ltEnat/= ltnW.
+rewrite ln_powR mulrCA mulVf//.
+  by rewrite mulr1 lnK ?posrE.
+by rewrite gt_eqF// -ln1 ltr_ln ?posrE// ?ltr1n// ltr0n ltnW.
 Qed.
 
 Lemma Exp_oppr n x : Exp n (- x) = (Exp n x)^-1.
-Proof. by rewrite /Exp mulNr expRN. Qed.
+Proof. by rewrite /Exp -powRN. Qed.
 
-Lemma Exp_gt0 n x : 0 < Exp n x. Proof. by rewrite /Exp expR_gt0. Qed.
+Lemma Exp_gt0 n x : 0 < n -> 0 < Exp n x. Proof. by move=> ?; rewrite /Exp powR_gt0. Qed.
 
-Lemma Exp_ge0 n x : 0 <= Exp n x. Proof. exact/ltW/Exp_gt0. Qed.
+Lemma Exp_ge0 n x : 0 <= Exp n x. Proof. by rewrite /Exp powR_ge0. Qed.
 
-Lemma Exp_increasing n x y : (1 < n)%N -> x < y -> Exp n x < Exp n y.
-Proof. by move=> ? ?; rewrite ltr_expR// ltr_pM2r// ln_gt0// ltr1n. Qed.
+Lemma Exp_increasing n x y : 1 < n -> x < y -> Exp n x < Exp n y.
+Proof.
+move=> n1 xy; rewrite /Exp /powR ifF; last first.
+  by apply/negbTE; rewrite gt_eqF// (lt_trans _ n1).
+rewrite ifF//; last first.
+  by apply/negbTE; rewrite gt_eqF// (lt_trans _ n1).
+by rewrite ltr_expR// ltr_pM2r// ln_gt0// ltr1n.
+Qed.
 
-Lemma Exp_le_increasing n x y : (1 < n)%N -> x <= y -> Exp n x <= Exp n y.
+Lemma Exp_le_increasing n x y : 1 < n -> x <= y -> Exp n x <= Exp n y.
 Proof.
-move=> n1; rewrite /Exp le_eqVlt => /predU1P[->//|].
-by move/Exp_increasing => x_y; exact/ltW/x_y.
+by move=> n1 xy; rewrite /Exp ler_powR// ltW.
 Qed.
 
 End Exp.
 
-Hint Extern 0 (0 < Exp _ _) => solve [exact/Exp_gt0] : core.
-
 Hint Extern 0 (0 <= Exp _ _) => solve [exact/Exp_ge0] : core.
 
 Section log.
@@ -188,6 +196,18 @@ move=> x0; rewrite logexp1E ler_wpM2r// ?invr_ge0//= ?(ltW (@ln2_gt0 _))//.
 exact/ln_id_cmp.
 Qed.
 
+Lemma log_powR (a x : R) : log (a `^ x) = x * log a.
+Proof.
+by rewrite /log /Log ln_powR// mulrA.
+Qed.
+
+Lemma log_increasing (a b : R) : 0 < a -> a < b -> log a < log b.
+Proof.
+move=> Ha a_b.
+rewrite /log /Log prednK// ltr_pmul2r ?invr_gt0 ?ln2_gt0//.
+by rewrite ltr_ln ?posrE// (lt_trans _ a_b).
+Qed.
+
 End log.
 
 Lemma log_prodr_sumr_mlog {R : realType} {A : finType} (f : A -> R) s :