diff --git a/information_theory/joint_typ_seq.v b/information_theory/joint_typ_seq.v
index e19d44f5..3299d1e4 100644
--- a/information_theory/joint_typ_seq.v
+++ b/information_theory/joint_typ_seq.v
@@ -110,7 +110,9 @@ Definition Nup (x : R) := `| Num.floor x |.+1.
 Lemma Nup_gt x : x < (Nup x)%:R.
 Proof.
 apply: (lt_le_trans (floorD1_gt x)).
-by rewrite /Nup -intrD1 -natr1 lerD // natr_absz ler_int ler_norm.
+rewrite /Nup.
+rewrite [leLHS](_ : _ = (Num.Def.floor x)%:~R + 1%:~R); last by rewrite intrD1.
+by rewrite -natr1 lerD // natr_absz ler_int ler_norm.
 Qed.
 
 Definition JTS_1_bound :=
diff --git a/information_theory/source_coding_vl_converse.v b/information_theory/source_coding_vl_converse.v
index eb6ce626..3e5262d6 100644
--- a/information_theory/source_coding_vl_converse.v
+++ b/information_theory/source_coding_vl_converse.v
@@ -2,6 +2,7 @@
 (* Copyright (C) 2025 infotheo authors, license: LGPL-2.1-or-later            *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint matrix.
 From mathcomp Require Import archimedean lra ring.
+From mathcomp Require Import mathcomp_extra.
 From mathcomp Require Import unstable contra reals normedtype sequences exp.
 Require Import ssr_ext ssralg_ext bigop_ext realType_ext realType_ln.
 Require Import fdist proba entropy divergence log_sum source_code.
@@ -779,8 +780,9 @@ apply: (@le_trans _ _ ((x ^ 2 / 2 - 1) * eps * n%:R)); last first.
   rewrite /m /x.
   rewrite lerBlDr.
   rewrite (le_trans (ltW (floorD1_gt _)))//.
-  rewrite natr_absz intrD1 ler_int.
-  by rewrite lerD2r ler_norm.
+  rewrite natr_absz.
+  rewrite [leRHS](_ : _ = (`|floor (expR (m' eps))| + 1)%:~R); last by rewrite intrD1.
+  by rewrite ler_int lerD2r ler_norm.
 rewrite logM//; last exact: mpos.
 rewrite -(ler_pM2r ln2_gt0).
 rewrite mulrDl -(mulrA (ln alp)) (mulVf ln2_neq0).