1 files changed, 5 insertions, 4 deletions
diff --git a/flocq/Core/FLT.v b/flocq/Core/FLT.v
index 7301328d..ee0b5d90 100644
--- a/flocq/Core/FLT.v
+++ b/flocq/Core/FLT.v
@@ -18,9 +18,10 @@ COPYING file for more details.
 *)
 
 (** * Floating-point format with gradual underflow *)
-Require Import Raux Defs Round_pred Generic_fmt Float_prop.
-Require Import FLX FIX Ulp Round_NE.
-Require Import Psatz.
+
+From Coq Require Import ZArith Reals Psatz.
+
+Require Import Zaux Raux Defs Round_pred Generic_fmt Float_prop FLX FIX Ulp Round_NE.
 
 Section RND_FLT.
 
@@ -336,7 +337,7 @@ rewrite <- bpow_plus.
 right; apply f_equal.
 replace (e - 1 + (1 - prec))%Z with (e - prec)%Z by ring.
 apply Z.max_l; simpl.
-assert (emin+prec-1 < e)%Z; try lia.
+cut (emin+prec-1 < e)%Z. lia.
 apply lt_bpow with beta.
 apply Rle_lt_trans with (1:=Hx).
 now apply He.