diff --git a/src/Core/Fcore_generic_fmt.v b/src/Core/Fcore_generic_fmt.v
index d47513a0024c83abdc5f549b9f519c44ba45421a..7f45f528556638f54009360aef2967228e994854 100644
--- a/src/Core/Fcore_generic_fmt.v
+++ b/src/Core/Fcore_generic_fmt.v
@@ -303,7 +303,7 @@ Qed.
 
 Theorem canonic_exp_ge:
   forall prec,
-  (forall e, (e-prec <= fexp e)%Z) ->
+  (forall e, (e-fexp e <= prec)%Z) ->
   (* OK with FLX, FLT and FTZ *)
   forall x, generic_format x ->
   (Rabs x < bpow (prec + canonic_exponent x))%R.