diff --git a/information_theory/channel_coding_converse.v b/information_theory/channel_coding_converse.v
index e1bfdb9c..930cae3c 100644
--- a/information_theory/channel_coding_converse.v
+++ b/information_theory/channel_coding_converse.v
@@ -64,11 +64,9 @@ apply ler_wpM2l.
   by rewrite exprn_ge0//.
 set Vmax := [arg max_(V > _) _]%O.
 rewrite /success_factor_bound /exp_cdiv.
-case : ifP => Hcase; last first.
-  by rewrite mul0r Exp_ge0.
-rewrite -exp.powRD; last first.
-  by rewrite pnatr_eq0 implybT.
-rewrite exp.ler_powR ?ler1n//.
+case : ifP => Hcase; last by rewrite mul0r powR_ge0.
+rewrite -powRD; last by rewrite pnatr_eq0 implybT.
+rewrite ler_powR ?ler1n//.
 rewrite -mulrDr 2!mulNr.
 rewrite lerNr opprK; apply/ler_wpM2l; first exact/ler0n.
 have {}Hcase : Pmax |- Vmax << W.
@@ -105,7 +103,7 @@ Theorem channel_coding_converse : exists n0,
 Proof.
 case: (channel_coding_converse_gen minRate_cap set_of_I_has_ubound) => Delta [Delta_pos HDelta].
 pose K := (#|A| + #|A| * #|B|)%nat.
-pose n0 := 2 ^+ K * K.+1`!%:R / ((Delta * exp.ln 2) ^+ K.+1) / epsilon.
+pose n0 := 2 ^+ K * K.+1`!%:R / ((Delta * ln 2) ^+ K.+1) / epsilon.
 exists n0 => n M c HM n0_n HminRate.
 have Rlt0n : 0 < n%:R :> R.
   apply: (lt_trans _ n0_n).
@@ -114,7 +112,7 @@ have Rlt0n : 0 < n%:R :> R.
   rewrite -mulrA mulr_gt0 ?exprn_gt0//.
   rewrite divr_gt0// ?ltr0n ?fact_gt0//.
   rewrite exprn_gt0//.
-  by rewrite mulr_gt0// exp.ln_gt0// ltr1n.
+  by rewrite mulr_gt0// ln_gt0// ltr1n.
 destruct n as [|n'].
   by rewrite ltxx in Rlt0n.
 set n := n'.+1.
@@ -134,7 +132,7 @@ rewrite -2!mulrA.
 set aux := _%:R * (_ * _).
 have aux_gt0 : 0 < aux.
   rewrite mulr_gt0 ?ltr0n ?fact_gt0// divr_gt0//.
-  by rewrite invr_gt0// exprn_gt0// mulr_gt0// exp.ln_gt0 ?ltr1n.
+  by rewrite invr_gt0// exprn_gt0// mulr_gt0// ln_gt0 ?ltr1n.
 apply (@le_trans _ _ ((n.+1%:R / n%:R) ^+ K * aux)); last first.
   rewrite ler_pM2r//.
   rewrite lerXn2r ?nnegrE ?divr_ge0//.
@@ -142,11 +140,11 @@ apply (@le_trans _ _ ((n.+1%:R / n%:R) ^+ K * aux)); last first.
   by rewrite -[in leRHS]mulrC mulr_natr mulr2n -natr1 lerD2l ler1n.
 rewrite expr_div_n -mulrA ler_wpM2l//.
 - by rewrite exprn_ge0.
-- rewrite -lef_pV2 ?posrE ?Exp_gt0//; last first.
+- rewrite -lef_pV2 ?posrE ?powR_gt0//; last first.
     by rewrite mulr_gt0// invr_gt0 exprn_gt0.
   rewrite -powRN mulNr opprK.
-  have nDeltaln2 : 0 < n%:R * Delta * exp.ln 2.
-    by rewrite mulr_gt0// ?exp.ln_gt0 ?ltr1n// mulr_gt0//.
+  have nDeltaln2 : 0 < n%:R * Delta * ln 2.
+    by rewrite mulr_gt0// ?ln_gt0 ?ltr1n// mulr_gt0//.
   rewrite /exp.powR(* TODO *) pnatr_eq0/=.
   apply/ltW.
   apply: (le_lt_trans _ (exp_strict_lb K.+1 nDeltaln2)) => {nDeltaln2}.
diff --git a/information_theory/channel_coding_direct.v b/information_theory/channel_coding_direct.v
index cc5c67a0..6ee4577b 100644
--- a/information_theory/channel_coding_direct.v
+++ b/information_theory/channel_coding_direct.v
@@ -28,8 +28,8 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Import Prenex Implicits.
 
-Local Open Scope ring_scope.
 Local Open Scope fdist_scope.
+Local Open Scope ring_scope.
 Local Open Scope jtyp_seq_scope.
 Local Open Scope channel_code_scope.
 Local Open Scope channel_scope.
@@ -49,9 +49,9 @@ Lemma f0 g : 0 <= f g. Proof. by rewrite ffunE prodr_ge0. Qed.
 Lemma f1 : \sum_(g in {ffun M -> 'rV[A]_n}) f g = 1.
 Proof.
 under eq_bigr do rewrite ffunE /=.
-rewrite -(bigA_distr_bigA (fun _ v => (P `^ n) v)) /=.
+rewrite -(bigA_distr_bigA (fun _ => (P `^ n)%fdist)) /=.
 rewrite [RHS](_ : _ = \prod_(m0 : M | xpredT m0) 1); last by rewrite big1.
-by apply eq_bigr => _ _; rewrite (FDist.f1 (P `^ n)).
+by apply eq_bigr => _ _; rewrite (FDist.f1 (P `^ n)%fdist).
 Qed.
 
 Definition d : {fdist encT A M n} := locked (FDist.make f0 f1).
@@ -253,7 +253,7 @@ Definition epsilon0_condition r epsilon epsilon0 :=
 Definition frac_part (x : R) := x - (Num.floor x)%:~R.
 Definition n_condition r epsilon0 n :=
   (O < n)%nat /\ - log epsilon0 / epsilon0 < n%:R /\
-  frac_part (2 `^ (r *+ n))%R = 0 /\ (JTS_1_bound P W epsilon0 <= n)%nat.
+  frac_part (2 `^ (r *+ n)) = 0 /\ (JTS_1_bound P W epsilon0 <= n)%nat.
 
 Definition cal_E M n epsilon (f : encT A M n) m :=
   [set vb | prod_rV (f m, vb) \in `JTS P W n epsilon].
@@ -294,7 +294,7 @@ transitivity (\sum_(j : {ffun 'I_k -> 'rV[_]_n}) \prod_(m < k) (Q `^ _)%fdist (j
   - move=> i /=; apply/esym/eqP/eq_from_tnth => j.
     by rewrite tnth_fgraph ffunE enum_valK.
   - by move=> i _; apply eq_bigr => j _; rewrite ffunE /= tcastE -enum_rank_ord.
-rewrite -(bigA_distr_bigA (fun m xn => (Q `^ _) xn)) /= big_const.
+rewrite -(bigA_distr_bigA (fun _ => (Q `^ _)%fdist)) /= big_const.
 by rewrite FDist.f1 iter_mulr mulr1 expr1n.
 Qed.
 
@@ -686,14 +686,12 @@ have [k Hk] : exists k, log k.+1%:R / n%:R = r :> R.
   rewrite prednK; last first.
     rewrite absz_gt0; apply/eqP => Habs.
     rewrite /frac_part Habs subr0 in Hn2.
-    suff : false => //.
-    have := @Exp_gt0 R 2 (rate r *+ n).
-    by rewrite Hn2 ltxx; apply.
+    by move/eqP : Hn2; apply/negP; rewrite gt_eqF// powR_gt0.
   rewrite eqr_divr_mulr; last by rewrite (eqr_nat R n 0) -lt0n.
   rewrite -[in LHS]mulrz_nat natz gez0_abs.
     move/subr0_eq: Hn2 => <-.
     by rewrite /log ExpK // mulr_natr.
-  by rewrite floor_ge0 Exp_ge0.
+  by rewrite floor_ge0 powR_ge0.
 set M : finType := 'I_k.+1.
 exists M.
 split; first by rewrite /= card_ord.
@@ -779,7 +777,7 @@ rewrite (_ : _ + _ = - n%:R * (`I(P, W) - log #| M |%:R / n%:R - 3 * epsilon0));
   by case: Hn; rewrite -(ltr_nat R) => /lt0r_neq0.
 rewrite (_ : _ / _ = rate r); last by rewrite -Hk card_ord.
 apply (@lt_trans _ _ (2 `^ (- n%:R * epsilon0))).
-  apply Exp_increasing; first by rewrite (ltr_nat R 1 2).
+  rewrite gt1_ltr_powRr ?ltr1n//.
   rewrite -mulr_natr -mulNr.
   rewrite -2!mulrA ltr_nM2l ?oppr_lt0 //.
   rewrite ltr_pM2l; last by case: Hn; rewrite (ltr_nat R 0 n).
@@ -807,7 +805,7 @@ Lemma exists_frac_part (P : nat -> Prop) : (exists n, P n) ->
   forall num den, (0 < num)%nat -> (0 < den)%nat ->
   (forall n m, (n <= m)%nat -> P n -> P m) ->
   exists n, P n /\
-    frac_part (2 `^ (n%:R * (log num%:R / den%:R)))%R = 0.
+    frac_part (2 `^ (n%:R * (log num%:R / den%:R))) = 0.
 Proof.
 case=> n Pn num den Hden HP.
 exists (n * den)%nat.
@@ -816,7 +814,7 @@ split.
   by rewrite -{1}(muln1 n) leq_mul2l HP orbC.
 rewrite natrM -mulrA (mulrCA den%:R) mulrV // ?mulr1; last first.
   by rewrite unitfE lt0r_neq0 // (ltr_nat R 0).
-rewrite /frac_part mulrC exp.powRrM -/(2 `^ _)%R.
+rewrite /frac_part mulrC powRrM.
 rewrite (LogK (n:=2)) // ?ltr0n // powR_mulrn ?ler0n // -natrX.
 by rewrite floorK ?subrr // intr_nat.
 Qed.
@@ -891,7 +889,7 @@ case: (random_coding_good_code He Hepsilon0 Hn) =>
 case: (good_code_sufficient_condition H) => f Hf.
 exists n, M, (mkCode f (jtdec P W epsilon0 f)); split => //.
 rewrite /CodeRate M_k -mulrz_nat natz gez0_abs; last first.
-  by rewrite floor_ge0 Exp_ge0.
+  by rewrite floor_ge0 powR_ge0.
 case: Hn => Hn [_] [].
 rewrite /frac_part => /subr0_eq <- _.
 rewrite /log ExpK // -(mulr_natr (rate r)) mulrK //.
diff --git a/information_theory/conditional_divergence.v b/information_theory/conditional_divergence.v
index d79f777c..35307da0 100644
--- a/information_theory/conditional_divergence.v
+++ b/information_theory/conditional_divergence.v
@@ -20,8 +20,8 @@ Unset Strict Implicit.
 Import Prenex Implicits.
 
 Local Open Scope reals_ext_scope.
-Local Open Scope ring_scope.
 Local Open Scope fdist_scope.
+Local Open Scope ring_scope.
 Local Open Scope entropy_scope.
 Local Open Scope channel_scope.
 Local Open Scope divergence_scope.
@@ -33,7 +33,7 @@ Import Order.TTheory GRing.Theory Num.Theory.
 Section conditional_dominance.
 Variables (A B : finType) (V W : `Ch(A, B)) (P : {fdist A}).
 
-Definition cdom_by := forall a, P a != 0%R -> V a `<< W a.
+Definition cdom_by := forall a, P a != 0 -> V a `<< W a.
 
 Lemma dom_by_cdom_by : (P `X V) `<< (P `X W) <-> cdom_by.
 Proof.
@@ -178,8 +178,7 @@ transitivity (\prod_(a : A) \prod_(b : B) \prod_(i < n)
 apply eq_bigr => a _; apply eq_bigr => b _.
 rewrite num_co_occ_alt -sum1_card.
 rewrite (@big_morph _ _ (fun x => W a b ^+ x) 1 *%R O addn) //; last first.
-  move=> * /=.
-  by rewrite exprD.
+  by move=> * /=; rewrite exprD.
 rewrite [in RHS]big_mkcond.
 apply eq_bigr => i _.
 case: ifP.
@@ -204,7 +203,7 @@ Hypothesis Hn : n != O.
    the conditional divergence and the condition entropy *)
 
 Lemma dmc_cdiv_cond_entropy :
-  (W ``(y | x) = 2 `^ (- n%:R * (D(V || W | P) + `H(V | P))))%R.
+  W ``(y | x) = 2 `^ (- n%:R * (D(V || W | P) + `H(V | P))).
 Proof.
 rewrite dmc_cdiv_cond_entropy_aux cond_entropy_chanE2.
 rewrite /cdiv /entropy -big_split /=.
@@ -239,17 +238,13 @@ case/boolP : (V a b == 0) => [/eqP|] Vab0.
     by rewrite expr0 Vab0 !(mulr0,mul0r,addr0,add0r,oppr0,powRr0).
   move: Hy; rewrite in_set => /forallP/(_ a)/forallP/(_ b)/eqP => ->.
   by rewrite jtype_0_jtypef.
-rewrite -exp.powR_mulrn ?Exp_ge0//.
-rewrite -exp.powRrM//.
-congr (exp.powR _ _).
-(*rewrite -exp2_pow; congr exp2.*)
+rewrite -powR_mulrn ?powR_ge0// -powRrM//.
+congr (_ `^ _).
 rewrite -mulrN -mulrDr mulrA.
 rewrite logM; last 2 first.
   by rewrite -fdist_gt0.
-  rewrite invr_gt0.
-  by rewrite -fdist_gt0.
-rewrite logV; last first.
-  by rewrite -fdist_gt0.
+  by rewrite invr_gt0 -fdist_gt0.
+rewrite logV; last by rewrite -fdist_gt0.
 rewrite addrAC subrr add0r.
 rewrite mulrN 3!mulNr opprK.
 rewrite mulrC.
@@ -277,17 +272,20 @@ Variable W : `Ch*(A, B).
 
 Definition exp_cdiv :=
   if (type.d P) |- V <<b W
-  then (2 `^ (- n%:R * D(V || W | P)))%R
+  then 2 `^ (- n%:R * D(V || W | P))
   else 0.
 
-Lemma exp_cdiv_left (H : P |- V << W) : (exp_cdiv = 2 `^ (- n%:R * D(V || W | P)))%R.
+Lemma exp_cdiv_left (H : P |- V << W) : exp_cdiv = 2 `^ (- n%:R * D(V || W | P)).
 Proof.
 rewrite /exp_cdiv.
 suff : (type.d P) |- V <<b W by move=> ->.
 apply/forallP => a; apply/implyP => Pa0.
-apply/forall_inP => b /eqP Wab; by rewrite (dominatesE (H _ Pa0)).
+by apply/forall_inP => b /eqP Wab; rewrite (dominatesE (H _ Pa0)).
 Qed.
 
+Lemma exp_cdiv_ge0 : 0 <= exp_cdiv.
+Proof. by rewrite /exp_cdiv; case: ifPn => // _; rewrite powR_ge0. Qed.
+
 End cdiv_specialized.
 
 Section dmc_cdiv_cond_entropy_spec.
@@ -308,8 +306,7 @@ Lemma dmc_exp_cdiv_cond_entropy :
 Proof.
 rewrite /exp_cdiv.
 case : ifP => Hcase.
-- rewrite -exp.powRD; last first.
-   by rewrite pnatr_eq0 implybT.
+- rewrite -powRD; last by rewrite pnatr_eq0 implybT.
   rewrite -mulrDr.
   apply dmc_cdiv_cond_entropy => //.
   (* TODO: lemma? *)
diff --git a/information_theory/joint_typ_seq.v b/information_theory/joint_typ_seq.v
index b7872084..a421c148 100644
--- a/information_theory/joint_typ_seq.v
+++ b/information_theory/joint_typ_seq.v
@@ -189,7 +189,7 @@ have : (JTS_1_bound <= n)%nat ->
     rewrite lerBlDr addrC -lerBlDr; apply: le_trans.
     by rewrite Pr_to_cplt setCK.
   move=> Hn.
-  rewrite [in X in _ <= X](_ : epsilon = epsilon / 3 + epsilon / 3 + epsilon / 3)%R; last by field.
+  rewrite [in X in _ <= X](_ : epsilon = epsilon / 3 + epsilon / 3 + epsilon / 3); last by field.
   move: Hn; rewrite 2!geq_max => /andP[Hn1 /andP[Hn2 Hn3]].
   rewrite !Pr_DMC_rV_prod.
   apply lerD; first by apply lerD; [exact: HnP | exact: HnPW].
@@ -231,7 +231,7 @@ apply (@le_trans _ _ (\sum_(i | i \in `JTS P W n epsilon)
   - rewrite fdist_prodE ler_pM //.
       by case/andP: (typical_sequence1_JTS iJTS).
     by case/andP: (typical_sequence1_JTS' iJTS).
-  - by rewrite mulr_ge0 // Exp_ge0.
+  - by rewrite mulr_ge0 ?powR_ge0.
   - by rewrite prod_rVK eqxx andbC.
 rewrite (_ : \sum_(_ | _) _ =
   #| `JTS P W n epsilon|%:R *
@@ -239,7 +239,7 @@ rewrite (_ : \sum_(_ | _) _ =
   last by rewrite big_const iter_addr addr0 -mulr_natl mulrA.
 apply (@le_trans _ _ (2 `^ (n%:R * (`H( P , W ) + epsilon)) *
   2 `^ (- n%:R * (`H P - epsilon)) * 2 `^ (- n%:R * (`H( P `o W ) - epsilon)))).
-  by rewrite !ler_wpM2r ?Exp_ge0 // JTS_sup.
+  by rewrite !ler_wpM2r ?powR_ge0 // JTS_sup.
 apply/eqW.
 rewrite -!powRD; try by rewrite (@eqr_nat R 2 0) implybT.
 rewrite /mutual_info_chan !mulrDr !mulrNN; congr exp.powR.
diff --git a/information_theory/jtypes.v b/information_theory/jtypes.v
index 802027d1..550d85ba 100644
--- a/information_theory/jtypes.v
+++ b/information_theory/jtypes.v
@@ -36,8 +36,8 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Import Prenex Implicits.
 
-Local Open Scope R_scope.
 Local Open Scope channel_scope.
+Local Open Scope ring_scope.
 
 Import Num.Theory.
 
@@ -52,8 +52,8 @@ Record t : predArgType := mk {
   sum_f : \sum_(a in A) \sum_(b in B) f a b == n ;
   c_f : forall a b, c a b = let row := \sum_(b in B) f a b in
                             if row == O
-                            then #|B|%:R^-1%R
-                            else ((f a b)%:R / row%:R)%R }.
+                            then #|B|%:R^-1
+                            else (f a b)%:R / row%:R }.
 
 End def.
 End JType.
@@ -97,22 +97,22 @@ Definition nneg_fun_of_pre_jtype (A B : finType) n
 pose pf := fun a => [ffun b : B =>
   let ln := (\sum_(b1 in B) (f a b1))%nat in
   if ln == O
-    then #|B|%:R^-1%R
-    else (f a b)%:R / ln%:R]%R.
+    then #|B|%:R^-1
+    else (f a b)%:R / ln%:R].
 exact: pf.
 Defined.
 
 Definition nneg_fun_of_pre_jtype_ge0 (A B : finType) (Bnot0 : (0 < #|B|)%nat) n
-  (f : {ffun A -> {ffun B -> 'I_n.+1}}) :
-  (forall a b, 0 <= nneg_fun_of_pre_jtype f a b)%R.
+    (f : {ffun A -> {ffun B -> 'I_n.+1}}) a b :
+  0 <= nneg_fun_of_pre_jtype f a b.
 Proof.
-move=> a b.
 rewrite /nneg_fun_of_pre_jtype ffunE.
 case: ifPn => [_ | Hcase].
-- by rewrite invr_ge0//.
-- by rewrite divr_ge0//.
+- by rewrite invr_ge0.
+- by rewrite divr_ge0.
 Qed.
 
+(* TODO: move *)
 Import GRing.Theory Order.POrderTheory.
 
 Definition chan_of_jtype (A B : finType) (Anot0 : (0 < #|A|)%nat)
@@ -121,8 +121,8 @@ Definition chan_of_jtype (A B : finType) (Anot0 : (0 < #|A|)%nat)
 set pf := fun a b =>
   let ln := (\sum_(b1 in B) (f a b1))%nat in
   if ln == O
-  then #|B|%:R^-1%R
-  else ((f a b)%:R / ln%:R)%R : Rdefinitions.R.
+  then #|B|%:R^-1
+  else ((f a b)%:R / ln%:R) : Rdefinitions.R.
 refine (@Channel1.mkChan A B _ Anot0) => a.
 apply: (@FDist.make _ _ (@nneg_fun_of_pre_jtype _ _ n f a)).
   move=> b.
@@ -281,16 +281,16 @@ have -> : tmp = pmap (fun f =>
 eq_ind_r
                                      (eq^~ (if (\sum_(b0 in B) sval f a b0)%nat == 0%N
                                             then #|B|%:R^-1
-                                            else (sval f a b)%:R / (\sum_(b0 in B) sval f a b0)%:R))%R
+                                            else (sval f a b)%:R / (\sum_(b0 in B) sval f a b0)%:R))
                                      (erefl
                                         (if (\sum_(b0 in B) sval f a b0)%nat == 0%N
-                                         then #|B|%:R^-1%R
-                                         else (sval f a b)%:R / (\sum_(b0 in B) sval f a b0)%:R))%R
+                                         then #|B|%:R^-1
+                                         else (sval f a b)%:R / (\sum_(b0 in B) sval f a b0)%:R))
                                      (ffunE
                                         (fun b0 : B =>
                                          if (\sum_(b1 in B) sval f a b1)%nat == 0%N
-                                         then #|B|%:R^-1%R
-                                         else (sval f a b0)%:R / (\sum_(b1 in B) sval f a b1)%:R) b)%R
+                                         then #|B|%:R^-1
+                                         else (sval f a b0)%:R / (\sum_(b1 in B) sval f a b1)%:R) b)
                                              (*(if \sum_(b0 in B) (sval f a) b0 == 0%N
                                               then / #|B|%:R
                                               else
@@ -339,7 +339,7 @@ exfalso.
 move/negP : abs; apply.
 apply/negP.
 rewrite invr_eq0.
-rewrite (_ : 0%R = 0%:R)%R//.
+rewrite (_ : 0%R = 0%:R)//.
 by rewrite eqr_nat.
 Qed.
 
@@ -378,7 +378,7 @@ have [tmp Htmp] : {f : {ffun A -> {ffun B -> 'I_n.+1}} |
 have Htmp' : (forall a b,
         (chan_of_jtype Anot0 Bnot0 tmp) a b =
         (let ln := \sum_(b0 in B) (tmp a) b0 in
-         if ln == 0 then #|B|%:R^-1%R else (((tmp a) b)%:R / ln%:R)%R)).
+         if ln == 0 then #|B|%:R^-1 else ((tmp a) b)%:R / ln%:R)).
   by move=> a0 b0; rewrite ffunE.
 exists (@JType.mk _ _ _ (chan_of_jtype Anot0 Bnot0 tmp) tmp Htmp Htmp').
 by rewrite inE.
@@ -651,7 +651,6 @@ Proof. by rewrite ltnS -(H Hta) (bigD1 b) // leq_addr. Qed.
 End row_num_occ_sect.
 
 Section take_shell_row_num_occ.
-
 Variables A B : finType.
 Variable n : nat.
 Variable V : P_ n ( A , B).
@@ -664,7 +663,7 @@ Local Open Scope nat_scope.
 
 Definition type_of_row (a : A) (Ha : N(a | ta) != 0) : P_ N(a | ta) ( B ).
 pose f := [ffun b => Ordinal (ctyp_element_ub Hrow_num_occ Hta a b)].
-pose d := [ffun b => ((f b)%:R / N(a | ta)%:R)%R : Rdefinitions.R].
+pose d := [ffun b => ((f b)%:R / N(a | ta)%:R) : Rdefinitions.R].
 assert (d0 : forall b, (0 <= d b)%mcR).
   move=> b.
   by rewrite /d /= ffunE mulr_ge0// invr_ge0.
@@ -674,7 +673,7 @@ assert (d1 : (\sum_(b : B) d b)%R = 1%R).
   rewrite -natr_sum.
   set lhs := \sum_i _.
   suff -> : lhs = N(a | ta).
-    by rewrite mulfV // (_ : 0%R = 0%:R)%R// eqr_nat.
+    by rewrite mulfV // (_ : 0%R = 0%:R)// eqr_nat.
   rewrite /lhs /f /= -[in X in _ = X](Hrow_num_occ Hta a).
   apply eq_bigr => b _; by rewrite ffunE.
 by apply (@type.mkType _ _ (FDist.make d0 d1) f) => b; rewrite ffunE.
@@ -728,7 +727,7 @@ apply/andP; split.
   have Ht2 : tval t = drop (sum_num_occ ta k) (take (sum_num_occ ta k.+1) tb).
     rewrite Ht {1}sum_num_occ_rec take_drop take_takel; last by rewrite addnC.
     by rewrite addnC sum_num_occ_rec.
-  congr (_ %:R / _%:R)%R.
+  congr (_ %:R / _%:R).
   exact/esym/num_occ_num_co_occ.
 Qed.
 
@@ -805,36 +804,34 @@ Hypothesis ta_sorted : sorted (@le_rank _) ta.
 Hypothesis Bnot0 : (0 < #|B|)%nat.
 
 Lemma card_shell_leq_exp_entropy :
-  (#| V.-shell ta |%:R <= (2%:R:Rdefinitions.R) `^ (n%:R * `H(V | P)))%R.
+  #| V.-shell ta |%:R <= (2%:R:Rdefinitions.R) `^ (n%:R * `H(V | P)).
 Proof.
 rewrite cond_entropy_chanE2.
-apply (@le_trans _ _ (\prod_ ( i < #|A|) card_type_of_row Hta Vctyp i)%:R)%R.
+apply (@le_trans _ _ (\prod_ ( i < #|A|) card_type_of_row Hta Vctyp i)%:R).
 - rewrite ler_nat.
   by apply/card_shelled_tuples_leq_prod_card.
 - rewrite Exp2_pow.
   rewrite natr_prod.
-  rewrite (@big_morph _ _ (fun r : Rdefinitions.R => (((2%:R:Rdefinitions.R) `^ r) ^+ n)%R) 1%R GRing.mul _ GRing.add _); last 2 first.
+  rewrite (@big_morph _ _ (fun r : Rdefinitions.R => (((2%:R:Rdefinitions.R) `^ r) ^+ n)) 1%R GRing.mul _ GRing.add _); last 2 first.
     move=> a b /=; rewrite -!Exp2_pow mulrDr.
     rewrite powRD//.
-    rewrite (_ : 0%R = 0%:R)%R//.
-    rewrite eqr_nat.
-    by rewrite implybT.
+    rewrite (_ : 0%R = 0%:R)//.
+    by rewrite eqr_nat implybT.
     by rewrite powRr0 expr1n.
   rewrite (reindex_onto (fun x => enum_rank x) (fun y => enum_val y)) => [|i _]; last by rewrite enum_valK.
   rewrite (_ : \prod_(j | enum_val (enum_rank j) == j) _ =
-               \prod_(j : A) (card_type_of_row Hta Vctyp (enum_rank j))%:R)%R; last first.
+               \prod_(j : A) (card_type_of_row Hta Vctyp (enum_rank j))%:R); last first.
       apply eq_bigl => a; rewrite enum_rankK; by apply/eqP.
   apply ler_prod => a aA.
   apply/andP; split => //.
   rewrite -Exp2_pow mulrA.
   rewrite /card_type_of_row; case: Bool.bool_dec => [e|/Bool.eq_true_not_negb e].
-    rewrite -[X in (X <= _)%R](powRr0 2).
-    rewrite Exp_le_increasing ?ltr1n// !mulr_ge0//.
-    exact: entropy_ge0.
+    rewrite -[X in X <= _](powRr0 2).
+    by rewrite gt1_ler_powRr ?ltr1n// !mulr_ge0//; exact: entropy_ge0.
   set pta0 := type_of_row Hta Vctyp _.
-  rewrite (_ : (_ `^ _ = (2%:R:Rdefinitions.R) `^ (N(a | ta)%:R * `H pta0))%R).
-    by rewrite -[in X in (_ <= _ _ (X * _))%R](enum_rankK a); apply card_typed_tuples.
-  congr (_ `^ _)%R.
+  rewrite (_ : _ `^ _ = (2%:R:Rdefinitions.R) `^ (N(a | ta)%:R * `H pta0)).
+    by rewrite -[in X in _ <= _ _ (X * _)](enum_rankK a); apply card_typed_tuples.
+  congr (_ `^ _).
   f_equal.
   + by rewrite -type_fun_type // (type_numocc Hta).
   + rewrite /entropy.
@@ -1127,10 +1124,10 @@ Variable n' : nat.
 Let n := n'.+1.
 Variable V : P_ n ( A , B ).
 
-Definition f := [ffun b => ((\sum_(a in A) (JType.f V) a b)%:R / n%:R)%R : Rdefinitions.R].
+Definition f := [ffun b => (\sum_(a in A) (JType.f V) a b)%:R / n%:R : Rdefinitions.R].
 
-Lemma f0 (b : B) : (0 <= f b)%mcR.
-Proof. rewrite ffunE; apply/ divr_ge0; [exact/ler0n | exact: ler0n]. Qed.
+Lemma f0 (b : B) : (0 <= f b)%R.
+Proof. rewrite ffunE; apply/divr_ge0; [exact/ler0n | exact: ler0n]. Qed.
 
 Lemma f1 : (\sum_(b in B) f b = 1)%R.
 Proof.
@@ -1138,7 +1135,7 @@ under eq_bigr do rewrite ffunE /=.
 rewrite -big_distrl /=.
 rewrite -natr_sum exchange_big /=.
 move/eqP : (JType.sum_f V) => ->; rewrite mulfV //.
-by rewrite (_ : 0%R = 0%:R)%R// eqr_nat.
+by rewrite (_ : 0%R = 0%:R)// eqr_nat.
 Qed.
 
 Definition d : {fdist B} := FDist.make f0 f1.
@@ -1201,10 +1198,10 @@ case: ifP => [/eqP |] Hcase.
   move/forallP/(_ b) : Hcase.
   move/implyP/(_ Logic.eq_refl)/eqP => ->.
   by rewrite mul0r.
-- rewrite -mulrA sum_V; congr (_ * _)%R.
+- rewrite -mulrA sum_V; congr *%R.
   move: Hta; rewrite in_set => /forallP/(_ a)/eqP ->.
   rewrite mulrA mulVf ?div1r// -sum_V.
-  by rewrite (_ : 0%R = 0%:R)%R// eqr_nat Hcase.
+  by rewrite (_ : 0%R = 0%:R)// eqr_nat Hcase.
 Qed.
 
 Lemma output_type_out_entropy : `H (`tO( V )) = `H(P `o V).
@@ -1227,7 +1224,8 @@ Hypothesis Hta : ta \in T_{P}.
 Hypothesis Vctyp : V \in \nu^{B}(P).
 Hypothesis Bnot0 : (0 < #|B|)%nat.
 
-Lemma card_shelled_tuples : (#| V.-shell ta |%:R <= (2%:R:Rdefinitions.R) `^ (n%:R * `H(V | P)))%R.
+Lemma card_shelled_tuples :
+  (#| V.-shell ta |%:R <= (2%:R:Rdefinitions.R) `^ (n%:R * `H(V | P)))%R.
 Proof.
 case: (tuple_exist_perm_sort (@le_rank A) ta) => /= s Hta'.
 have H : sort (@le_rank _) ta =
@@ -1272,7 +1270,7 @@ assert (Hf : \sum_(a in A) \sum_(b in B) f a b == n).
 assert (Htmp' : (forall a b,
         (chan_of_jtype Anot0 Bnot0 f) a b =
         (let ln := (\sum_(b0 in B) (f a) b0)%nat in
-         if ln == O then #|B|%:R^-1 else (((f a) b)%:R / ln%:R))%R)).
+         if ln == O then #|B|%:R^-1 else (((f a) b)%:R / ln%:R)))).
   by move=> a b; rewrite ffunE.
 exact (@JType.mk _ _ _ (chan_of_jtype Anot0 Bnot0 f) f Hf Htmp').
 Defined.
@@ -1311,7 +1309,7 @@ exists (num_co_occ_jtype ta tb).-shell ta.
     rewrite Hta'.
     move=> /(congr1 (fun x => x * n%:R)%R).
     rewrite -!mulrA mulVf ?mulr1; last first.
-      by rewrite (_ : 0%R = 0%:R)%R// eqr_nat.
+      by rewrite (_ : 0%R = 0%:R)// eqr_nat.
     by move=> /eqP; rewrite eqr_nat => /eqP.
 - rewrite in_set.
   apply/forallP => a. apply/forallP => b.
diff --git a/information_theory/shannon_fano.v b/information_theory/shannon_fano.v
index fa14a773..d57bc836 100644
--- a/information_theory/shannon_fano.v
+++ b/information_theory/shannon_fano.v
@@ -1,8 +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 all_algebra archimedean.
-From mathcomp Require Import Rstruct reals exp.
-Require Import ssrZ ssr_ext realType_logb realType_ext fdist bigop_ext.
+From mathcomp Require Import Rstruct mathcomp_extra reals exp.
+Require Import ssr_ext bigop_ext realType_logb realType_ext fdist.
 Require Import entropy kraft.
 
 (******************************************************************************)
@@ -40,8 +40,6 @@ Section shannon_fano_def.
 
 Variables (A T : finType) (P : {fdist A}).
 
-Local Open Scope zarith_ext_scope.
-
 Definition is_shannon_fano (f : Encoding.t A T) :=
   forall s, size (f s) = `| Num.ceil (Log #|T|%:R (P s)^-1%R) |%N.
 
@@ -75,17 +73,16 @@ rewrite H.
 have Pi0 : 0 < P i by rewrite lt0r Pr0/=.
 apply (@le_trans _ _ (#|T|%:R `^ (- Log #|T|%:R (P i)^-1))%R); last first.
   by rewrite LogV// opprK natn LogK// card_ord.
-rewrite pow_Exp; last by rewrite card_ord.
-rewrite powRN card_ord lef_pV2// ?posrE ?Exp_gt0//.
-rewrite Exp_le_increasing// ?ltr1n//.
-rewrite (le_trans (mathcomp_extra.ceil_ge _))//.
+rewrite -powR_mulrn; last by rewrite card_ord.
+rewrite powRN card_ord lef_pV2// ?posrE ?powR_gt0//.
+rewrite gt1_ler_powRr ?ltr1n//.
+rewrite (le_trans (ceil_ge _))//.
 by rewrite natr_absz// ler_int ler_norm.
 Qed.
 
 End shannon_fano_is_kraft.
 
 Section average_length.
-
 Variables (A T : finType) (P : {fdist A}).
 Variable f : {ffun A -> seq T}. (* encoding function *)
 
@@ -127,19 +124,18 @@ apply (@lt_le_trans _ _ (\sum_(x in A) P x * (- Log #|T|%:R (P x) + 1))).
   by rewrite -log1 ler_log// ?posrE// -fdist_gt0.
 under eq_bigr do rewrite mulrDr mulr1 mulrN.
 rewrite big_split /= FDist.f1 lerD2r.
-rewrite le_eqVlt; apply/orP; left; apply/eqP.
+apply/eqW.
 rewrite /entropy big_morph_oppr; apply eq_bigr => i _.
-by rewrite card_ord /log//.
+by rewrite card_ord.
 Qed.
 
 End shannon_fano_suboptimal.
 
 (* wip *)
 Section kraft_code_is_shannon_fano.
-
 Variables (A : finType) (P : {fdist A}).
 
-Variable (t' : nat).
+Variable t' : nat.
 Let n := #|A|.-1.+1.
 Let t := t'.+2.
 Let T := 'I_t.
diff --git a/information_theory/source_coding_fl_converse.v b/information_theory/source_coding_fl_converse.v
index c7b94370..97640caf 100644
--- a/information_theory/source_coding_fl_converse.v
+++ b/information_theory/source_coding_fl_converse.v
@@ -131,13 +131,12 @@ apply (@le_trans _ _ (2%R `^ n%:R)%R).
     by rewrite ler_nat; exact/leq_imset_card.
   rewrite cardsT card_mx /= card_bool mul1n.
   by rewrite powR_mulrn// natrX.
-apply Exp_le_increasing => //; rewrite ?ltr1n//.
+rewrite gt1_ler_powRr ?ltr1n//.
 rewrite /e0 [X in _ <= _ * X](_ : _ = r); last by field.
 rewrite -(@ler_pM2r _ (r^-1)) => //; last first.
-  rewrite invr_gt0//.
-  by case/andP : Hr.
+  by rewrite invr_gt0//; case/andP : Hr.
 rewrite -mulrA mulfV ?mulr1; last first.
-  by case/andP : Hr => r0 _; rewrite gt_eqF//.
+  by case/andP : Hr => r0 _; rewrite gt_eqF.
 rewrite (le_trans _ Hk)//.
 by rewrite /SrcConverseBound le_max lexx orbT.
 Qed.
@@ -200,26 +199,22 @@ apply/(le_trans step3); rewrite lerD//.
     by rewrite ltrNl oppr0 ltr0n.
   rewrite mulrA mulrN !mulNr opprK divff ?pnatr_eq0// mul1r => H2.
   have := FDist.ge0 (P `^ k.+1) i.
-  rewrite le_eqVlt => /predU1P[<-|Pki0].
-    by rewrite Exp_ge0.
-  rewrite -ler_log; last 2 first.
-    by rewrite posrE.
-    by rewrite posrE Exp_gt0.
+  rewrite le_eqVlt => /predU1P[<-|Pki0]; first by rewrite powR_ge0.
+  rewrite -ler_log ?posrE ?powR_gt0//.
   by rewrite log_powR log2 mulr1.
 Qed.
 
 Lemma step5 : 1 - (esrc(P , sc)) <= delta + 2 `^ (- k.+1%:R * (e0 - delta)).
 Proof.
 apply (@le_trans _ _ (delta + #| no_failure |%:R * 2 `^ (- k.+1%:R * (`H P - delta)))).
-- apply/(le_trans step4); rewrite lerD2l ler_wpM2r// ?Exp_ge0// ler_nat.
+- apply/(le_trans step4); rewrite lerD2l ler_wpM2r ?powR_ge0// ler_nat.
   exact/subset_leqif_cards/subsetIl.
 - rewrite lerD2l.
   apply (@le_trans _ _ (2 `^ (k.+1%:R * (`H P - e0)) * 2 `^ (- k.+1%:R * (`H P - delta))));
     last first.
     rewrite -powRD; last by rewrite pnatr_eq0 implybT.
-    rewrite Exp_le_increasing ?ltr1n//.
-    lra.
-  by rewrite ler_wpM2r ?Exp_ge0//; exact no_failure_sup.
+    by rewrite gt1_ler_powRr ?ltr1n//; lra.
+  by rewrite ler_wpM2r ?powR_ge0//; exact: no_failure_sup.
 Qed.
 
 Lemma step6 : 1 - 2 * delta <= esrc(P , sc).
@@ -227,9 +222,7 @@ Proof.
 have H : (2 `^ (- k.+1%:R * (e0 - delta)) <= delta)%R; last first.
   suff : 1 - (esrc(P , sc)) <= delta + delta by move=> *; lra.
   by apply/(le_trans step5); rewrite lerD2l.
-rewrite -ler_log; last 2 first.
-  by rewrite posrE Exp_gt0.
-  by rewrite posrE Hdelta.
+rewrite -ler_log ?posrE ?powR_gt0 ?Hdelta//.
 rewrite log_powR log2 mulr1.
 rewrite -(@ler_pM2r _ ((e0 - delta)^-1)) ?invr_gt0 ?subr_gt0//; last first.
   rewrite /e0 /delta /r.
@@ -259,7 +252,7 @@ have H1 : lambda / 2 <= 2^-1 * (1 - epsilon).
   by rewrite /lambda mulrC ge_min lexx.
 apply: (@minr_case_strong _ ((`H P - r) / 2) (lambda / 2)
   (fun x => x <= 2^-1 * (1 - epsilon))) => //.
-by move/le_trans; apply.
+by move/le_trans; exact.
 Qed.
 
 End source_coding_converse'.
@@ -267,14 +260,14 @@ End source_coding_converse'.
 Section source_coding_converse.
 Variables (A : finType) (P : {fdist A}).
 
-Theorem source_coding_converse : forall epsilon, 0 < epsilon < 1 ->
+Theorem source_coding_converse epsilon : 0 < epsilon < 1 ->
   forall nu de : nat, 0 < (nu%:R / de.+1%:R : Rdefinitions.R) < `H P ->
     forall n k (sc : scode_fl A k.+1 n),
       SrcRate sc = nu%:R / de%:R ->
       SrcConverseBound P nu de n epsilon <= k.+1%:R ->
       epsilon <= esrc(P , sc).
 Proof.
-move=> epsilon Hespilon nu de r_HP n k sc r_sc Hk_bound.
+move=> espilon01 nu de r_HP n k sc r_sc Hk_bound.
 exact: (@source_coding_converse' _ _ nu de).
 Qed.
 
diff --git a/information_theory/source_coding_fl_direct.v b/information_theory/source_coding_fl_direct.v
index 214c67d1..6ce4b8c7 100644
--- a/information_theory/source_coding_fl_direct.v
+++ b/information_theory/source_coding_fl_direct.v
@@ -20,8 +20,8 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Import Prenex Implicits.
 
-Local Open Scope ring_scope.
 Local Open Scope fdist_scope.
+Local Open Scope ring_scope.
 
 Section encoder_and_decoder.
 Let R := Rdefinitions.R.
@@ -111,12 +111,12 @@ Local Open Scope reals_ext_scope.
 Section source_coding_direct'.
 Let R := Rdefinitions.R.
 Variables (A : finType) (P : R.-fdist A) (num den : nat).
-Let r : R := (num%:R / den.+1%:R)%R.
+Let r : R := num%:R / den.+1%:R.
 Hypothesis Hr : `H P < r.
 Variable epsilon : R.
 Hypothesis epsilon01 : 0 < epsilon < 1.
 
-Definition lambda := minr (r - `H P)%R epsilon.
+Definition lambda := minr (r - `H P) epsilon.
 
 Lemma lambda_gt0 : 0 < lambda.
 Proof.
@@ -153,7 +153,6 @@ have [?|?] := leP (r - `H P) epsilon.
 - lra.
 Qed.
 
-Local Open Scope fdist_scope.
 Local Open Scope typ_seq_scope.
 
 Theorem source_coding' : exists sc : scode_fl A k n,
@@ -171,41 +170,41 @@ exists (mkScode F PHI); split.
   field.
   by rewrite !nat1r/= !gt_eqF//=.
 set lhs := esrc(_, _).
-suff -> : lhs = (1 - Pr (P `^ k)%fdist (`TS P k (lambda / 2)))%R.
+suff -> : lhs = 1 - Pr (P `^ k)%fdist (`TS P k (lambda / 2)).
   rewrite lerBlDr addrC -lerBlDr.
-  apply (@le_trans _ _ (1 - lambda / 2)%R).
+  apply (@le_trans _ _ (1 - lambda / 2)).
     by rewrite lerD2l lerNr opprK; exact: lambda2_epsilon.
   exact: (Pr_TS_1 lambda2_gt0).
 rewrite /lhs {lhs} /SrcErrRate /Pr /=.
 set lhs := \sum_(_ | _ ) _.
 suff -> : lhs = \sum_(x in 'rV[A]_k | x \notin S) (P `^ k)%fdist x.
-  have : forall a b : R, (a + b = 1 -> b = 1 - a)%R by move=> ? ? <-; field.
+  have : forall a b : R, a + b = 1 -> b = 1 - a by move=> ? ? <-; field.
   apply.
-  rewrite -[X in _ = X](Pr_cplt (P `^ k) (`TS P k (lambda / 2))).
-  congr (_ + _)%R.
+  rewrite -[X in _ = X](Pr_cplt (P `^ k)%fdist (`TS P k (lambda / 2))).
+  congr +%R.
   by apply: eq_bigl => ta /=; rewrite !inE.
 rewrite {}/lhs; apply eq_bigl => //= i.
 rewrite inE /=; apply/negPn/negPn.
 - suff H : def \in S by move/eqP/phi_f; tauto.
   exact: (TS_0_is_typ_seq lambda2_gt0 lambda2_lt1 Hk).
 - suff S_2n : (#| S | < expn 2 n)%nat by move/(f_phi def S_2n)/eqP.
-  suff card_S_bound : (#| S |%:R < 2 `^ (k%:R * r))%R.
-    rewrite -(ltr_nat R) -natrXE natrX pow_Exp ?ler0n//.
-    suff : n%:R = (k%:R * r)%R by move=> ->.
+  suff card_S_bound : #| S |%:R < 2 `^ (k%:R * r).
+    rewrite -(ltr_nat R) -natrXE natrX -powR_mulrn ?ler0n//.
+    suff : n%:R = k%:R * r by move=> ->.
     rewrite /n /k /r.
     by rewrite !natrM mulrCA -mulrA divff ?mulr1 ?pnatr_eq0// mulrC.
-  suff card_S_bound : 1 + #| S |%:R <= (2 `^ (k%:R * r))%R by lra.
-  suff card_S_bound : 1 + #| S |%:R <= (2 `^ (k%:R * (`H P + lambda)))%R.
+  suff card_S_bound : 1 + #| S |%:R <= 2 `^ (k%:R * r) by lra.
+  suff card_S_bound : 1 + #| S |%:R <= 2 `^ (k%:R * (`H P + lambda)).
     apply: le_trans; first exact: card_S_bound.
-    by rewrite Exp_le_increasing// ?ltr1n// ler_wpM2l// Hlambdar.
-  apply (@le_trans _ _ (2 `^ (k%:R * (lambda / 2) + k%:R * (`H P + lambda / 2)))%R); last first.
+    by rewrite gt1_ler_powRr ?ltr1n// ler_wpM2l// Hlambdar.
+  apply (@le_trans _ _ (2 `^ (k%:R * (lambda / 2) + k%:R * (`H P + lambda / 2)))); last first.
     rewrite -mulrDr addrC -addrA.
-    rewrite (_ : forall a, a / 2 + a / 2 = a)%R; last by move=> ?; field.
+    rewrite (_ : forall a, a / 2 + a / 2 = a); last by move=> ?; field.
     by rewrite lexx.
-  apply (@le_trans _ _ (2 `^ (1 + k%:R * (`H P + lambda / 2)))%R); last first.
-    rewrite Exp_le_increasing ?ltr1n// lerD2r//.
+  apply (@le_trans _ _ (2 `^ (1 + k%:R * (`H P + lambda / 2)))); last first.
+    rewrite gt1_ler_powRr ?ltr1n// lerD2r//.
     move: Hdelta; rewrite ge_max => /andP[_ Hlambda].
-    rewrite -(@ler_pM2r _ (2 / lambda)%R); last first.
+    rewrite -(@ler_pM2r _ (2 / lambda)); last first.
       by rewrite divr_gt0//; exact: lambda_gt0.
     rewrite mul1r -mulrA.
     rewrite -[in leRHS]invf_div// mulVf ?mulr1//.
@@ -215,19 +214,12 @@ rewrite inE /=; apply/negPn/negPn.
     exact: TS_sup.
     rewrite /S.
   apply (@le_trans _ _ (2 `^ (k%:R * (`H P + lambda / 2)) +
-                        2 `^ (k%:R * (`H P + lambda / 2)))%R).
-  + rewrite lerD2r.
-    rewrite [leLHS](_ : 1 = 2 `^ 0)%R; last by rewrite powRr0.
-    rewrite Exp_le_increasing ?ltr1n//.
-    apply mulr_ge0; first exact: ler0n.
-    apply addr_ge0; first exact: entropy_ge0.
-    by rewrite ltW//; exact: lambda2_gt0.
-  + rewrite -mulr2n.
-    rewrite -mulr_natl.
-    rewrite powRD.
-    rewrite ler_pM2r ?Exp_gt0//.
-    rewrite exp.le1r_powR ?ler1n//.
-    by rewrite pnatr_eq0 implybT.
+                        2 `^ (k%:R * (`H P + lambda / 2)))).
+  + rewrite lerD2r -[leLHS](powRr0 2).
+    rewrite ler_powR ?ler1n// mulr_ge0// addr_ge0//; first exact: entropy_ge0.
+    by rewrite divr_ge0// ltW// lambda_gt0.
+  + rewrite -mulr2n -mulr_natl powRD; last by rewrite pnatr_eq0 implybT.
+    by rewrite ler_pM2r ?powR_gt0// powRr1.
 Qed.
 
 End source_coding_direct'.
@@ -237,7 +229,8 @@ Variables (A : finType) (P : {fdist A}).
 
 Theorem source_coding_direct epsilon : 0 < epsilon < 1 ->
   forall nu de : nat, `H P < nu%:R / de.+1%:R ->
-    exists k n (sc : scode_fl A k n), SrcRate sc = nu%:R/de.+1%:R /\ esrc(P , sc) <= epsilon.
+    exists k n (sc : scode_fl A k n), SrcRate sc = nu%:R/de.+1%:R /\
+                                      esrc(P , sc) <= epsilon.
 Proof.
 move=> Heps nu de HP_r.
 exists (k P nu de epsilon), (n P nu de epsilon).
diff --git a/information_theory/source_coding_vl_converse.v b/information_theory/source_coding_vl_converse.v
index f484efd3..6f39d4d4 100644
--- a/information_theory/source_coding_vl_converse.v
+++ b/information_theory/source_coding_vl_converse.v
@@ -1,10 +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 ssralg ssrnum ssrint matrix archimedean.
-(*Require Import Reals.*)
-From mathcomp Require Import lra ring.
-From mathcomp Require Import Rstruct reals sequences.
-Require Import (*ssrR Reals_ext*) realType_ext realType_logb ssr_ext ssralg_ext bigop_ext.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint matrix.
+From mathcomp Require Import archimedean lra ring.
+From mathcomp Require Import Rstruct reals sequences exp.
+Require Import ssr_ext ssralg_ext bigop_ext realType_ext realType_logb.
 Require Import fdist proba entropy divergence log_sum source_code.
 
 (******************************************************************************)
@@ -198,7 +197,7 @@ Local Open Scope vec_ext_scope.
 Section Entropy_lemma.
 Variables (A : finType) (P : {fdist A}) (n : nat).
 
-Lemma entropy_TupleFDist : `H (P `^ n) = n%:R * `H P.
+Lemma entropy_TupleFDist : `H (P `^ n)%fdist = n%:R * `H P.
 Proof.
 elim:n=>[|n0 IH].
   rewrite mul0r /entropy /= big1 ?oppr0 // => i _.
@@ -233,7 +232,7 @@ rewrite [LHS](_ :_ = \sum_(i | i \in A) P i * log (P i) *
     by rewrite lt0r eq_sym rmul_non0; apply/prodr_ge0 => ?.
   by rewrite logM//.
 rewrite (_ : \sum_(j in 'rV_n0) _ = 1); last first.
-  rewrite -[RHS](FDist.f1 (P `^ n0)).
+  rewrite -[RHS](FDist.f1 (P `^ n0)%fdist).
   by apply eq_bigr => i _; rewrite fdist_rVE.
 rewrite -big_distrl /= mulr1 [in RHS]addrC; congr (_ + _).
 rewrite -big_distrl /= FDist.f1 mul1r; apply eq_bigr => i _.
@@ -252,7 +251,7 @@ Hypothesis f_uniq : uniquely_decodable f.
 
 Let Xnon0 x : 0 <> X x.
 Proof.
-rewrite /X /=; have [/eqP|/eqP//] := eqVneq (0:R)%R (size (f x))%:R.
+rewrite /X /=; have [/eqP|/eqP//] := eqVneq (0:R) (size (f x))%:R.
 rewrite (_ : 0 = 0%:R)// eqr_nat => /eqP.
 move/esym/size0nil => fx_nil.
 move: (@f_uniq [::] ([:: x])).
@@ -687,7 +686,7 @@ Lemma apply_le_HN_logE_loge : `H P <= `E X  + log ((expR 1) * `E X).
 Proof.
 apply: (le_trans apply_max_HPN).
 rewrite lerD2l mulrC.
-rewrite (logM (EX_gt0 P f_uniq))// ?exp.expR_gt0//.
+rewrite (logM (EX_gt0 P f_uniq)) ?expR_gt0//.
 exact: le_entroPN_logeEX f_uniq.
 Qed.
 
@@ -701,17 +700,17 @@ Variable P : {fdist A}.
 Hypothesis f_uniq : uniquely_decodable f.
 
 Lemma converse_case1 : @E_leng_cw _ _ P f < n%:R * log #|A|%:R ->
-`H (P `^ n) <= @E_leng_cw _ _ P f + log ((expR 1) * n%:R * log #|A|%:R).
+`H (P `^ n)%fdist <= @E_leng_cw _ _ P f + log ((expR 1) * n%:R * log #|A|%:R).
 Proof.
-move=>H.
-apply: (le_trans (apply_le_HN_logE_loge (P `^ n) f_uniq)).
+move=> H.
+apply: (le_trans (apply_le_HN_logE_loge (P `^ n)%fdist f_uniq)).
 rewrite lerD2l//; apply: Log_increasing_le => //.
-  by apply/mulr_gt0; [exact/exp.expR_gt0 | exact/EX_gt0].
-rewrite -mulrA ler_wpM2l//; [exact/exp.expR_ge0|exact/ltW].
+  by rewrite mulr_gt0 ?expR_gt0// EX_gt0.
+by rewrite -mulrA ler_wpM2l ?expR_ge0// ltW.
 Qed.
 
 Lemma converse_case2 : n%:R * log #|A|%:R <= @E_leng_cw _ _ P f ->
- `H (P `^ n) <= @E_leng_cw _ _ P f.
+ `H (P `^ n)%fdist <= @E_leng_cw _ _ P f.
 Proof.
 move=> H; rewrite entropy_TupleFDist; apply: (le_trans _ H).
 by rewrite ler_wpM2l//; exact/entropy_max.
@@ -750,7 +749,7 @@ elim => /= [| ta1 sta1 IHsta1]; case => [| ta2 sta2] //=.
   exact/tuple_of_row_inj/eqP.
 Qed.
 
-Lemma ELC_TupleFDist : @E_leng_cw _ _ (P `^ n) fm = m%:R * @E_leng_cw _ _ P f.
+Lemma ELC_TupleFDist : @E_leng_cw _ _ (P `^ n)%fdist fm = m%:R * @E_leng_cw _ _ P f.
 Proof.
 rewrite /E_leng_cw /=  /fm.
 pose X := (fun x => x%:R : R) \o size \o f.
@@ -792,7 +791,7 @@ have X_Xm1_Xm2 : Xm2 \= X @+ Xm1.
     by apply eq_from_tnth => i; rewrite {i}(ord1 i) /= tnth_mktuple mxE.
   by rewrite /= cats0.
 rewrite (E_sum_2 X_Xm1_Xm2).
-rewrite -natr1 mulrDl -IH addrC; congr (_ + _)%R.
+rewrite -natr1 mulrDl -IH addrC; congr +%R.
   by rewrite /Xm1 -/fm1 /Ex tail_of_fdist_rV_fdist_rV.
 by rewrite -/X mul1r /Ex head_of_fdist_rV_fdist_rV.
 Qed.
@@ -801,7 +800,6 @@ End Extend_encoder.
 
 Section v_scode_converse'.
 Let R := Rdefinitions.R.
-
 Variables (A : finType) (P : {fdist A}).
 Variable n : nat.
 Variable f : encT A (seq bool) n.
@@ -867,30 +865,7 @@ apply: (@le_trans _ _ ((x ^ 2 / 2 - 1) * eps * n%:R)); last first.
   rewrite mulrC ler_wpM2r//.
   apply: (@le_trans _ _ (expR x - 1)).
     rewrite lerBlDr subrK (_ : 2 = (2 `!)%:R)//.
-From mathcomp Require Import topology normedtype exp.
-(* TODO: make a lemma out of this *)
-    rewrite exp.expRE.
-    rewrite (le_trans _ (nondecreasing_cvgn_le _ _ 3))//=.
-    - rewrite /pseries/= /series/=.
-      rewrite big_mkord big_ord_recr/=.
-      rewrite factE/= !muln1.
-      rewrite (mulrC 2^-1).
-      rewrite lerDr sumr_ge0// => i _.
-      by rewrite mulr_ge0 ?invr_ge0// exprn_ge0//.
-    - move=> a b ab.
-      rewrite /pseries/=.
-      rewrite /series/=.
-      rewrite -(subnKC ab).
-      rewrite /index_iota !subn0.
-      rewrite iotaD big_cat//=.
-      rewrite ler_wpDr// sumr_ge0// => i _.
-      by rewrite mulr_ge0 ?invr_ge0// exprn_ge0//.
-    - have := is_cvg_series_exp_coeff_pos xpos.
-      rewrite /exp_coeff /pseries.
-      rewrite /series/=.
-      under boolp.eq_fun do under eq_bigr do rewrite mulrC.
-      exact.
-(*; exact/(exp_lb 2)/pos_INR.*)
+    exact/ltW/exp_strict_lb.
   rewrite /m /x.
   rewrite lerBlDr.
   rewrite (le_trans (ltW (mathcomp_extra.lt_succ_floor _)))//.
@@ -898,8 +873,7 @@ From mathcomp Require Import topology normedtype exp.
   rewrite mathcomp_extra.intrD1 ler_int.
   rewrite lerD2r.
   by rewrite ler_norm.
-rewrite logM//; last first.
-  by apply: mpos.
+rewrite logM//; last exact: mpos.
 rewrite -(ler_pM2r ln2_gt0).
 rewrite mulrDl -(mulrA (ln alp)) (mulVf ln2_neq0).
 rewrite mulr1 -(mulrA _ (ln 2)^-1 _) (mulVf ln2_neq0).
@@ -1018,7 +992,6 @@ Qed.
 End v_scode_converse'.
 
 Section v_scode_converse.
-
 Variables (A : finType) (P : {fdist A}) (n : nat).
 Variable f : encT A (seq bool) n.
 Hypothesis f_uniq : uniquely_decodable f.
diff --git a/information_theory/success_decode_bound.v b/information_theory/success_decode_bound.v
index 81d6899b..91a2d323 100644
--- a/information_theory/success_decode_bound.v
+++ b/information_theory/success_decode_bound.v
@@ -306,9 +306,7 @@ rewrite (typed_success W Mnot0 tc).
 apply (@le_trans _ _ ( \sum_(V|V \in \nu^{B}(P)) exp_cdiv P V W *
     2 `^ (- n%:R *  +| log #|M|%:R * n%:R^-1 - `I(P, V) |))).
   apply: ler_sum => V Vnu.
-  rewrite -mulrA; apply ler_wpM2l.
-    rewrite /exp_cdiv; case : ifP => // ?.
-    by rewrite Exp_ge0.
+  rewrite -mulrA ler_wpM2l ?exp_cdiv_ge0//.
   by rewrite /success_factor mulrA; exact: success_factor_ub.
 apply (@le_trans _ _ (\sum_(V | V \in \nu^{B}(P)) exp_cdiv P Vmax W *
                     2 `^ (- n%:R * +| log #|M|%:R * n%:R^-1 - `I(P, Vmax)|))).
@@ -316,11 +314,9 @@ apply (@le_trans _ _ (\sum_(V | V \in \nu^{B}(P)) exp_cdiv P Vmax W *
   by move: (@arg_rmax2 _ (P_ n (A, B)) V0
     (fun V => exp_cdiv P V W * success_factor_bound M V P) V).
 rewrite big_const iter_addr /success_factor_bound addr0.
-rewrite -mulr_natr mulrC; apply ler_wpM2r.
-- apply mulr_ge0; last exact/Exp_ge0.
-  rewrite /exp_cdiv; case: ifP => // ?.
-  exact: Exp_ge0.
-by rewrite -natrX ler_nat card_nu.
+rewrite -mulr_natr mulrC ler_wpM2r//.
+- by rewrite mulr_ge0 ?powR_ge0 ?exp_cdiv_ge0.
+- by rewrite -natrX ler_nat card_nu.
 Qed.
 
 End typed_success_bound_sect.
diff --git a/information_theory/typ_seq.v b/information_theory/typ_seq.v
index 12f614c4..a0361bd0 100644
--- a/information_theory/typ_seq.v
+++ b/information_theory/typ_seq.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 matrix.
-From mathcomp Require Import reals lra exp.
+From mathcomp Require Import all_ssreflect ssralg ssrnum matrix lra.
+From mathcomp Require Import reals exp.
 Require Import ssr_ext realType_ext realType_logb.
 Require Import fdist proba entropy aep.
 
@@ -46,7 +46,7 @@ Context {R : realType}.
 Variables (A : finType) (P : R.-fdist A) (n : nat) (epsilon : R).
 
 Definition typ_seq (t : 'rV[A]_n) :=
-  (2 `^ (- n%:R * (`H P + epsilon)) <= (P `^ n)%fdist t <= 2 `^ (- n%:R * (`H P - epsilon)))%R.
+  2 `^ (- n%:R * (`H P + epsilon)) <= (P `^ n)%fdist t <= 2 `^ (- n%:R * (`H P - epsilon)).
 
 Definition set_typ_seq := [set ta | typ_seq ta].
 
@@ -56,21 +56,21 @@ Notation "'`TS'" := (set_typ_seq) : typ_seq_scope.
 
 Local Open Scope typ_seq_scope.
 
-Lemma set_typ_seq_incl {R : realType} (A : finType) (P : R.-fdist A) n epsilon : 0 <= epsilon ->
-  `TS P n (epsilon / 3) \subset `TS P n epsilon.
+Lemma set_typ_seq_incl {R : realType} (A : finType) (P : R.-fdist A) n epsilon :
+  0 <= epsilon -> `TS P n (epsilon / 3) \subset `TS P n epsilon.
 Proof.
 move=> e0.
 apply/subsetP => /= x.
-rewrite !inE /typ_seq => /andP[H2 H3] [:Htmp].
+rewrite !inE /typ_seq => /andP[H2 H3] [:e3e].
 apply/andP; split.
 - apply/(le_trans _ H2).
   rewrite ler_powR ?ler1n// !mulNr lerNr opprK; apply ler_wpM2l => //.
   rewrite lerD2l//.
-  abstract: Htmp.
+  abstract: e3e.
   by rewrite ler_pdivrMr// 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.
+  by rewrite lerD2l lerNr opprK; exact e3e.
 Qed.
 
 Section typ_seq_prop.
@@ -80,9 +80,10 @@ Variables (A : finType) (P : R.-fdist A) (epsilon : R) (n : nat).
 Lemma TS_sup : #| `TS P n epsilon |%:R <= 2 `^ (n%:R * (`H P + epsilon)).
 Proof.
 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.
+  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.
+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.
@@ -94,27 +95,24 @@ 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 <= - n.+1%:R^-1 * log ((P `^ n.+1)%fdist x) <= `H P + epsilon.
 Proof.
-rewrite inE /typ_seq.
-case/andP => H1 H2; apply/andP; split;
+rewrite inE /typ_seq => /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.
+    by rewrite (lt_le_trans _ H1)// powR_gt0.
+    by rewrite powR_gt0.
+  by rewrite mulNr powRN logV ?powR_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//.
+    have : 0 < 2 `^ (1 *- n.+1 * (`H P + epsilon)) by rewrite powR_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.
+  rewrite -ler_log ?posrE ?powR_gt0// in H1.
+  by rewrite mulNr powRN logV ?powR_gt0// log_powR log2 mulr1 mulrC in H1.
 Qed.
 
 End typ_seq_prop.
@@ -133,8 +131,7 @@ 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 => H _; apply/(lt_le_trans _ H).
-  by rewrite Exp_gt0//.
+  by case/andP : H => H _; apply/(lt_le_trans _ H); rewrite powR_gt0.
 set p := [set _ | _].
 rewrite Pr_to_cplt lerD2l lerNl opprK.
 have -> : Pr (P `^ n.+1)%fdist (~: p) =
@@ -194,7 +191,7 @@ Qed.
 Variable He1 : epsilon < 1.
 
 Lemma set_typ_seq_not0 : aep_bound P epsilon <= n.+1%:R ->
-  #| `TS P n.+1 epsilon | <> O.
+  #| `TS P n.+1 epsilon | != O.
 Proof.
 move/Pr_TS_1 => H.
 case/boolP : (#| `TS P n.+1 epsilon | == O) => [|Heq]; last by apply/eqP.
@@ -210,7 +207,7 @@ apply (@enum_val _ (pred_of_set (`TS P n.+1 epsilon))).
 have -> : #| `TS P n.+1 epsilon| = #| `TS P n.+1 epsilon|.-1.+1.
   rewrite prednK //.
   move/set_typ_seq_not0 in H.
-  rewrite lt0n; by apply/eqP.
+  by rewrite lt0n.
 exact ord0.
 Defined.
 
diff --git a/information_theory/types.v b/information_theory/types.v
index db05d260..19ad6e98 100644
--- a/information_theory/types.v
+++ b/information_theory/types.v
@@ -471,7 +471,7 @@ Lemma card_typed_tuples : (#| T_{ P } |%:R <= (2%:R:Rdefinitions.R) `^ (n%:R * `
 Proof.
 rewrite -(@invrK _ ((2%:R:Rdefinitions.R) `^ (n%:R * `H P))%R) -powRN -mulNr.
 set aux := - n%:R * `H P.
-rewrite -div1r ler_pdivlMr // {}/aux ?Exp_gt0//.
+rewrite -div1r ler_pdivlMr // {}/aux ?powR_gt0//.
 case/boolP : [exists x, x \in T_{P}] => x_T_P.
 - case/existsP : x_T_P => ta Hta.
   rewrite -(row_of_tupleK ta) in Hta.
diff --git a/lib/realType_logb.v b/lib/realType_logb.v
index e6a4953a..f0ef8138 100644
--- a/lib/realType_logb.v
+++ b/lib/realType_logb.v
@@ -35,14 +35,15 @@ Lemma ln2_ge0 : 0 <= ln 2 :> R. Proof. by rewrite ltW// ln2_gt0. Qed.
 Lemma lt_ln1Dx x : 0 < x -> ln (1 + x) < x.
 Proof.
 move=> x1.
-rewrite -ltr_expR lnK ?expR_gt1Dx//.
-  by rewrite gt_eqF//.
+rewrite -ltr_expR lnK.
+  by rewrite expR_gt1Dx// gt_eqF.
 by rewrite posrE addrC -ltrBlDr sub0r (le_lt_trans _ x1)// lerN10.
 Qed.
 
 Lemma ln_id_cmp x : 0 < x -> ln x <= x - 1.
 Proof.
-move=> x0; rewrite -{1}(GRing.subrK 1 x) addrC le_ln1Dx//.
+move=> x0.
+rewrite -{1}(subrK 1 x) addrC le_ln1Dx//.
 by rewrite -ltrBlDr opprK addrC subrr.
 Qed.
 
@@ -77,6 +78,7 @@ End xlnx.
 
 Section Log.
 Context {R : realType}.
+Implicit Type x : R.
 
 Definition Log (n : nat) x : R := ln x / ln n.-1.+1%:R.
 
@@ -114,10 +116,6 @@ Section Exp.
 Context {R : realType}.
 Implicit Type x : R.
 
-(* TODO: rename *)
-Lemma pow_Exp (x : R) n : (0 <= x) -> x ^+ n = x `^ n%:R.
-Proof. by move=> x0; rewrite powR_mulrn. Qed.
-
 (* TODO: rename *)
 Lemma Exp2_pow x n k : x `^ (k%:R * n) = (x `^ n) ^+ k.
 Proof. by rewrite -powR_mulrn ?powR_ge0// mulrC powRrM. Qed.
@@ -133,15 +131,8 @@ rewrite ln_powR mulrCA mulVf//.
 by rewrite gt_eqF// -ln1 ltr_ln ?posrE// ?ltr1n// ltr0n ltnW.
 Qed.
 
-(* TODO: rm *)
-Lemma Exp_gt0 n x : 0 < n -> 0 < n `^ x.
-Proof. by move=> ?; rewrite powR_gt0. Qed.
-
-(* TODO: rm *)
-Lemma Exp_ge0 n x : 0 <= n `^ x. Proof. by rewrite powR_ge0. Qed.
-
-(* TODO: rename *)
-Lemma Exp_increasing n x y : 1 < n -> x < y -> n `^ x < n `^ y.
+(* TODO: move to MCA? *)
+Lemma gt1_ltr_powRr (n : R) x y : 1 < n -> x < y -> n `^ x < n `^ y.
 Proof.
 move=> n1 xy; rewrite /powR ifF; last first.
   by apply/negbTE; rewrite gt_eqF// (lt_trans _ n1).
@@ -150,8 +141,8 @@ rewrite ifF//; last first.
 by rewrite ltr_expR// ltr_pM2r// ln_gt0// ltr1n.
 Qed.
 
-(* TODO: rename *)
-Lemma Exp_le_increasing n x y : 1 < n -> x <= y -> n `^ x <= n `^ y.
+(* TODO: move to MCA? *)
+Lemma gt1_ler_powRr (n : R) x y : 1 < n -> x <= y -> n `^ x <= n `^ y.
 Proof. by move=> n1 xy; rewrite ler_powR// ltW. Qed.
 
 (* TODO: move *)
@@ -160,13 +151,14 @@ Proof. by move=> ? ? /=; rewrite powRD// pnatr_eq0// implybT. Qed.
 
 End Exp.
 
-Hint Extern 0 (0 <= _ `^ _) => solve [exact/Exp_ge0] : core.
+Hint Extern 0 (0 <= _ `^ _) => solve [exact/powR_ge0] : core.
+Hint Extern 0 (0 < _ `^ _) => solve [exact/powR_gt0] : core.
 
 Section log.
 Context {R : realType}.
 Implicit Types x y : R.
 
-Definition log {R : realType} (x : R) := Log 2 x.
+Definition log x := Log 2 x.
 
 Lemma log1 : log 1 = 0 :> R. Proof. by rewrite /log Log1. Qed.
 
@@ -234,7 +226,7 @@ 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.
+Lemma log_powR (a : R) x : log (a `^ x) = x * log a.
 Proof.
 by rewrite /log /Log ln_powR// mulrA.
 Qed.
@@ -259,8 +251,7 @@ Proof.
 move=> f0 f0'.
 elim: s => [|h t ih].
   by rewrite !big_nil log1 oppr0.
-rewrite big_cons logM//; last first.
-  by apply/prodr_gt0 => a _.
+rewrite big_cons logM//; last exact/prodr_gt0.
 by rewrite [RHS]big_cons opprD ih.
 Qed.
 
@@ -272,7 +263,7 @@ Proof.
 move=> x0.
 case: n => [|n].
   by rewrite expr0 fact0 mul1r invr1 pexpR_gt1.
-rewrite exp.expRE.
+rewrite expRE.
 rewrite (lt_le_trans _ (nondecreasing_cvgn_le _ _ n.+2))//=.
 - rewrite /pseries/= /series/=.
   rewrite big_mkord big_ord_recr/=.
@@ -286,15 +277,11 @@ rewrite (lt_le_trans _ (nondecreasing_cvgn_le _ _ n.+2))//=.
   rewrite sumr_ge0// => i _.
   by rewrite mulr_ge0 ?invr_ge0// exprn_ge0// ltW.
 - move=> a b ab.
-  rewrite /pseries/=.
-  rewrite /series/=.
-  rewrite -(subnKC ab).
-  rewrite /index_iota !subn0.
-  rewrite iotaD big_cat//=.
+  rewrite /pseries/= /series/=.
+  rewrite -(subnKC ab) /index_iota !subn0 iotaD big_cat//=.
   rewrite ler_wpDr// sumr_ge0// => i _.
   by rewrite mulr_ge0 ?invr_ge0// exprn_ge0// ltW.
 - have := is_cvg_series_exp_coeff_pos x0.
-  rewrite /exp_coeff /pseries.
-  rewrite /series/=.
+  rewrite /exp_coeff /pseries /series/=.
   by under boolp.eq_fun do under eq_bigr do rewrite mulrC.
 Qed.