aboutsummaryrefslogtreecommitdiffstats
path: root/flocq/Prop/Plus_error.v
diff options
context:
space:
mode:
Diffstat (limited to 'flocq/Prop/Plus_error.v')
-rw-r--r--flocq/Prop/Plus_error.v10
1 files changed, 4 insertions, 6 deletions
diff --git a/flocq/Prop/Plus_error.v b/flocq/Prop/Plus_error.v
index 514d3aab..bf0b28cd 100644
--- a/flocq/Prop/Plus_error.v
+++ b/flocq/Prop/Plus_error.v
@@ -19,11 +19,9 @@ COPYING file for more details.
(** * Error of the rounded-to-nearest addition is representable. *)
-Require Import Psatz.
-Require Import Raux Defs Float_prop Generic_fmt.
-Require Import FIX FLX FLT Ulp Operations.
-Require Import Relative.
+From Coq Require Import ZArith Reals Psatz.
+Require Import Core Operations Relative.
Section Fprop_plus_error.
@@ -519,7 +517,7 @@ rewrite <- mag_minus1; try assumption.
unfold FLT_exp; apply bpow_le.
apply Z.le_trans with (2:=Z.le_max_l _ _).
destruct (mag beta x) as (n,Hn); simpl.
-assert (e + prec < n)%Z; try lia.
+cut (e + prec < n)%Z. lia.
apply lt_bpow with beta.
apply Rle_lt_trans with (1:=He).
now apply Hn.
@@ -567,7 +565,7 @@ unfold cexp.
rewrite <- mag_minus1 by easy.
unfold FLX_exp; apply bpow_le.
destruct (mag beta x) as (n,Hn); simpl.
-assert (e + prec < n)%Z; try lia.
+cut (e + prec < n)%Z. lia.
apply lt_bpow with beta.
apply Rle_lt_trans with (1:=He).
now apply Hn.