Update Flocq to 3.4.0 (#383)

29 files changed, 1840 insertions, 638 deletions

diff --git a/flocq/Calc/Bracket.v b/flocq/Calc/Bracket.v
index 83714e87..838cadfa 100644
--- a/flocq/Calc/Bracket.v
+++ b/flocq/Calc/Bracket.v
@@ -19,15 +19,19 @@ COPYING file for more details.
 
 (** * Locations: where a real number is positioned with respect to its rounded-down value in an arbitrary format. *)
 
+From Coq Require Import Lia.
 Require Import Raux Defs Float_prop.
+Require Import SpecFloatCompat.
+
+Notation location := location (only parsing).
+Notation loc_Exact := loc_Exact (only parsing).
+Notation loc_Inexact := loc_Inexact (only parsing).
 
 Section Fcalc_bracket.
 
 Variable d u : R.
 Hypothesis Hdu : (d < u)%R.
 
-Inductive location := loc_Exact | loc_Inexact : comparison -> location.
-
 Variable x : R.
 
 Definition inbetween_loc :=
@@ -233,7 +237,7 @@ apply Rplus_le_compat_l.
 apply Rmult_le_compat_r.
 now apply Rlt_le.
 apply IZR_le.
-omega.
+lia.
 (* . *)
 now rewrite middle_range.
 Qed.
@@ -246,7 +250,7 @@ Theorem inbetween_step_Lo :
 Proof.
 intros x k l Hx Hk1 Hk2.
 apply inbetween_step_not_Eq with (1 := Hx).
-omega.
+lia.
 apply Rcompare_Lt.
 assert (Hx' := inbetween_bounds _ _ (ordered_steps _) _ _ Hx).
 apply Rlt_le_trans with (1 := proj2 Hx').
@@ -255,7 +259,7 @@ rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l.
 apply Rcompare_not_Lt.
 rewrite <- mult_IZR.
 apply IZR_le.
-omega.
+lia.
 exact Hstep.
 Qed.
 
@@ -267,7 +271,7 @@ Theorem inbetween_step_Hi :
 Proof.
 intros x k l Hx Hk1 Hk2.
 apply inbetween_step_not_Eq with (1 := Hx).
-omega.
+lia.
 apply Rcompare_Gt.
 assert (Hx' := inbetween_bounds _ _ (ordered_steps _) _ _ Hx).
 apply Rlt_le_trans with (2 := proj1 Hx').
@@ -276,7 +280,7 @@ rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l.
 apply Rcompare_Lt.
 rewrite <- mult_IZR.
 apply IZR_lt.
-omega.
+lia.
 exact Hstep.
 Qed.
 
@@ -331,7 +335,7 @@ Theorem inbetween_step_any_Mi_odd :
 Proof.
 intros x k l Hx Hk.
 apply inbetween_step_not_Eq with (1 := Hx).
-omega.
+lia.
 inversion_clear Hx as [|l' _ Hl].
 now rewrite (middle_odd _ Hk) in Hl.
 Qed.
@@ -344,7 +348,7 @@ Theorem inbetween_step_Lo_Mi_Eq_odd :
 Proof.
 intros x k Hx Hk.
 apply inbetween_step_not_Eq with (1 := Hx).
-omega.
+lia.
 inversion_clear Hx as [Hl|].
 rewrite Hl.
 rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_r.
@@ -365,7 +369,7 @@ Theorem inbetween_step_Hi_Mi_even :
 Proof.
 intros x k l Hx Hl Hk.
 apply inbetween_step_not_Eq with (1 := Hx).
-omega.
+lia.
 apply Rcompare_Gt.
 assert (Hx' := inbetween_bounds_not_Eq _ _ _ _ Hx Hl).
 apply Rle_lt_trans with (2 := proj1 Hx').
@@ -387,7 +391,7 @@ Theorem inbetween_step_Mi_Mi_even :
 Proof.
 intros x k Hx Hk.
 apply inbetween_step_not_Eq with (1 := Hx).
-omega.
+lia.
 apply Rcompare_Eq.
 inversion_clear Hx as [Hx'|].
 rewrite Hx', <- Hk, mult_IZR.
@@ -433,10 +437,10 @@ now apply inbetween_step_Lo_not_Eq with (2 := H1).
 destruct (Zcompare_spec (2 * k) nb_steps) as [Hk1|Hk1|Hk1].
 (* . 2 * k < nb_steps *)
 apply inbetween_step_Lo with (1 := Hx).
-omega.
+lia.
 destruct (Zeven_ex nb_steps).
 rewrite He in H.
-omega.
+lia.
 (* . 2 * k = nb_steps *)
 set (l' := match l with loc_Exact => Eq | _ => Gt end).
 assert ((l = loc_Exact /\ l' = Eq) \/ (l <> loc_Exact /\ l' = Gt)).
@@ -490,7 +494,7 @@ now apply inbetween_step_Lo_not_Eq with (2 := H1).
 destruct (Zcompare_spec (2 * k + 1) nb_steps) as [Hk1|Hk1|Hk1].
 (* . 2 * k + 1 < nb_steps *)
 apply inbetween_step_Lo with (1 := Hx) (3 := Hk1).
-omega.
+lia.
 (* . 2 * k + 1 = nb_steps *)
 destruct l.
 apply inbetween_step_Lo_Mi_Eq_odd with (1 := Hx) (2 := Hk1).
@@ -499,7 +503,7 @@ apply inbetween_step_any_Mi_odd with (1 := Hx) (2 := Hk1).
 apply inbetween_step_Hi with (1 := Hx).
 destruct (Zeven_ex nb_steps).
 rewrite Ho in H.
-omega.
+lia.
 apply Hk.
 Qed.
 
@@ -612,7 +616,7 @@ clear -Hk. intros m.
 rewrite (F2R_change_exp beta e).
 apply (f_equal (fun r => F2R (Float beta (m * Zpower _ r) e))).
 ring.
-omega.
+lia.
 assert (Hp: (Zpower beta k > 0)%Z).
 apply Z.lt_gt.
 apply Zpower_gt_0.
@@ -622,7 +626,7 @@ rewrite 2!Hr.
 rewrite Zmult_plus_distr_l, Zmult_1_l.
 unfold F2R at 2. simpl.
 rewrite plus_IZR, Rmult_plus_distr_r.
-apply new_location_correct.
+apply new_location_correct; unfold F2R; simpl.
 apply bpow_gt_0.
 now apply Zpower_gt_1.
 now apply Z_mod_lt.
@@ -665,7 +669,7 @@ rewrite <- Hm in H'. clear -H H'.
 apply inbetween_unique with (1 := H) (2 := H').
 destruct (inbetween_float_bounds x m e l H) as (H1,H2).
 destruct (inbetween_float_bounds x m' e l' H') as (H3,H4).
-cut (m < m' + 1 /\ m' < m + 1)%Z. clear ; omega.
+cut (m < m' + 1 /\ m' < m + 1)%Z. clear ; lia.
 now split ; apply lt_F2R with beta e ; apply Rle_lt_trans with x.
 Qed.
 
diff --git a/flocq/Calc/Div.v b/flocq/Calc/Div.v
index 65195562..48e3bb51 100644
--- a/flocq/Calc/Div.v
+++ b/flocq/Calc/Div.v
@@ -19,6 +19,7 @@ COPYING file for more details.
 
 (** * Helper function and theorem for computing the rounded quotient of two floating-point numbers. *)
 
+From Coq Require Import Lia.
 Require Import Raux Defs Generic_fmt Float_prop Digits Bracket.
 
 Set Implicit Arguments.
@@ -80,7 +81,7 @@ assert ((F2R (Float beta m1 e1) / F2R (Float beta m2 e2) = IZR m1' / IZR m2' * b
   destruct (Zle_bool e (e1 - e2)) eqn:He' ; injection Hm ; intros ; subst.
   - split ; try easy.
     apply Zle_bool_imp_le in He'.
-    rewrite mult_IZR, IZR_Zpower by omega.
+    rewrite mult_IZR, IZR_Zpower by lia.
     unfold Zminus ; rewrite 2!bpow_plus, 2!bpow_opp.
     field.
     repeat split ; try apply Rgt_not_eq, bpow_gt_0.
@@ -88,8 +89,8 @@ assert ((F2R (Float beta m1 e1) / F2R (Float beta m2 e2) = IZR m1' / IZR m2' * b
   - apply Z.leb_gt in He'.
     split ; cycle 1.
     { apply Z.mul_pos_pos with (1 := Hm2).
-      apply Zpower_gt_0 ; omega. }
-    rewrite mult_IZR, IZR_Zpower by omega.
+      apply Zpower_gt_0 ; lia. }
+    rewrite mult_IZR, IZR_Zpower by lia.
     unfold Zminus ; rewrite bpow_plus, bpow_opp, bpow_plus, bpow_opp.
     field.
     repeat split ; try apply Rgt_not_eq, bpow_gt_0.
@@ -113,7 +114,7 @@ destruct (Z_lt_le_dec 1 m2') as [Hm2''|Hm2''].
   now apply IZR_neq, Zgt_not_eq.
   field.
   now apply IZR_neq, Zgt_not_eq.
-- assert (r = 0 /\ m2' = 1)%Z as [-> ->] by (clear -Hr Hm2'' ; omega).
+- assert (r = 0 /\ m2' = 1)%Z as [-> ->] by (clear -Hr Hm2'' ; lia).
   unfold Rdiv.
   rewrite Rmult_1_l, Rplus_0_r, Rinv_1, Rmult_1_r.
   now constructor.
@@ -150,10 +151,10 @@ unfold cexp.
 destruct (Zle_lt_or_eq _ _ H1) as [H|H].
 - replace (fexp (mag _ _)) with (fexp (e + 1)).
   apply Z.le_min_r.
-  clear -H1 H2 H ; apply f_equal ; omega.
+  clear -H1 H2 H ; apply f_equal ; lia.
 - replace (fexp (mag _ _)) with (fexp e).
   apply Z.le_min_l.
-  clear -H1 H2 H ; apply f_equal ; omega.
+  clear -H1 H2 H ; apply f_equal ; lia.
 Qed.
 
 End Fcalc_div.
diff --git a/flocq/Calc/Operations.v b/flocq/Calc/Operations.v
index 3416cb4e..ac93d412 100644
--- a/flocq/Calc/Operations.v
+++ b/flocq/Calc/Operations.v
@@ -17,7 +17,9 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 COPYING file for more details.
 *)
 
-(** Basic operations on floats: alignment, addition, multiplication *)
+(** * Basic operations on floats: alignment, addition, multiplication *)
+
+From Coq Require Import Lia.
 Require Import Raux Defs Float_prop.
 
 Set Implicit Arguments.
@@ -50,7 +52,7 @@ case (Zle_bool e1 e2) ; intros He ; split ; trivial.
 now rewrite <- F2R_change_exp.
 rewrite <- F2R_change_exp.
 apply refl_equal.
-omega.
+lia.
 Qed.
 
 Theorem Falign_spec_exp:
diff --git a/flocq/Calc/Round.v b/flocq/Calc/Round.v
index 5bde6af4..704a1ab2 100644
--- a/flocq/Calc/Round.v
+++ b/flocq/Calc/Round.v
@@ -19,6 +19,7 @@ COPYING file for more details.
 
 (** * Helper function for computing the rounded value of a real number. *)
 
+From Coq Require Import Lia.
 Require Import Core Digits Float_prop Bracket.
 
 Section Fcalc_round.
@@ -88,7 +89,7 @@ destruct Px as [Px|Px].
   destruct Bx as [Bx1 Bx2].
   apply lt_0_F2R in Bx1.
   apply gt_0_F2R in Bx2.
-  omega.
+  lia.
 Qed.
 
 (** Relates location and rounding. *)
@@ -585,7 +586,7 @@ apply Zlt_succ.
 rewrite Zle_bool_true with (1 := Hm).
 rewrite Zle_bool_false.
 now case Rlt_bool.
-omega.
+lia.
 Qed.
 
 Definition truncate_aux t k :=
@@ -674,7 +675,7 @@ unfold cexp.
 rewrite mag_F2R_Zdigits.
 2: now apply Zgt_not_eq.
 unfold k in Hk. clear -Hk.
-omega.
+lia.
 rewrite <- Hm', F2R_0.
 apply generic_format_0.
 Qed.
@@ -717,14 +718,14 @@ simpl.
 apply Zfloor_div.
 intros H.
 generalize (Zpower_pos_gt_0 beta k) (Zle_bool_imp_le _ _ (radix_prop beta)).
-omega.
+lia.
 rewrite scaled_mantissa_generic with (1 := Fx).
 now rewrite Zfloor_IZR.
 (* *)
 split.
 apply refl_equal.
 unfold k in Hk.
-omega.
+lia.
 Qed.
 
 Theorem truncate_correct_partial' :
@@ -744,7 +745,7 @@ destruct Zlt_bool ; intros Hk.
   now apply inbetween_float_new_location.
   ring.
 - apply (conj H1).
-  omega.
+  lia.
 Qed.
 
 Theorem truncate_correct_partial :
@@ -790,7 +791,7 @@ intros x m e l [Hx|Hx] H1 H2.
     destruct Zlt_bool.
       intros H.
       apply False_ind.
-      omega.
+      lia.
     intros _.
     apply (conj H1).
     right.
@@ -803,7 +804,7 @@ intros x m e l [Hx|Hx] H1 H2.
     rewrite mag_F2R_Zdigits with (1 := Zm).
     now apply Zlt_le_weak.
 - assert (Hm: m = 0%Z).
-  cut (m <= 0 < m + 1)%Z. omega.
+  cut (m <= 0 < m + 1)%Z. lia.
   assert (F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R as Hx'.
     apply inbetween_float_bounds with (1 := H1).
     rewrite <- Hx in Hx'.
@@ -1156,7 +1157,7 @@ exact H1.
 unfold k in Hk.
 destruct H2 as [H2|H2].
 left.
-omega.
+lia.
 right.
 split.
 exact H2.
@@ -1165,7 +1166,7 @@ inversion_clear H1.
 rewrite H.
 apply generic_format_F2R.
 unfold cexp.
-omega.
+lia.
 Qed.
 
 End Fcalc_round.
diff --git a/flocq/Calc/Sqrt.v b/flocq/Calc/Sqrt.v
index 8843d21e..4d267d21 100644
--- a/flocq/Calc/Sqrt.v
+++ b/flocq/Calc/Sqrt.v
@@ -19,6 +19,7 @@ COPYING file for more details.
 
 (** * Helper functions and theorems for computing the rounded square root of a floating-point number. *)
 
+From Coq Require Import Lia.
 Require Import Raux Defs Digits Generic_fmt Float_prop Bracket.
 
 Set Implicit Arguments.
@@ -86,7 +87,7 @@ assert (sqrt (F2R (Float beta m1 e1)) = sqrt (IZR m') * bpow e)%R as Hf.
 { rewrite <- (sqrt_Rsqr (bpow e)) by apply bpow_ge_0.
   rewrite <- sqrt_mult.
   unfold Rsqr, m'.
-  rewrite mult_IZR, IZR_Zpower by omega.
+  rewrite mult_IZR, IZR_Zpower by lia.
   rewrite Rmult_assoc, <- 2!bpow_plus.
   now replace (_ + _)%Z with e1 by ring.
   now apply IZR_le.
@@ -106,7 +107,7 @@ fold (Rsqr (IZR q)).
 rewrite sqrt_Rsqr.
 now constructor.
 apply IZR_le.
-clear -Hr ; omega.
+clear -Hr ; lia.
 (* .. r <> 0 *)
 constructor.
 split.
@@ -117,14 +118,14 @@ fold (Rsqr (IZR q)).
 rewrite sqrt_Rsqr.
 apply Rle_refl.
 apply IZR_le.
-clear -Hr ; omega.
+clear -Hr ; lia.
 apply sqrt_lt_1.
 rewrite mult_IZR.
 apply Rle_0_sqr.
 rewrite <- Hq.
 now apply IZR_le.
 apply IZR_lt.
-omega.
+lia.
 apply Rlt_le_trans with (sqrt (IZR ((q + 1) * (q + 1)))).
 apply sqrt_lt_1.
 rewrite <- Hq.
@@ -133,13 +134,13 @@ rewrite mult_IZR.
 apply Rle_0_sqr.
 apply IZR_lt.
 ring_simplify.
-omega.
+lia.
 rewrite mult_IZR.
 fold (Rsqr (IZR (q + 1))).
 rewrite sqrt_Rsqr.
 apply Rle_refl.
 apply IZR_le.
-clear -Hr ; omega.
+clear -Hr ; lia.
 (* ... location *)
 rewrite Rcompare_half_r.
 generalize (Rcompare_sqr (2 * sqrt (IZR (q * q + r))) (IZR q + IZR (q + 1))).
@@ -154,14 +155,14 @@ replace ((q + (q + 1)) * (q + (q + 1)))%Z with (4 * (q * q) + 4 * q + 1)%Z by ri
 generalize (Zle_cases r q).
 case (Zle_bool r q) ; intros Hr''.
 change (4 * (q * q + r) < 4 * (q * q) + 4 * q + 1)%Z.
-omega.
+lia.
 change (4 * (q * q + r) > 4 * (q * q) + 4 * q + 1)%Z.
-omega.
+lia.
 rewrite <- Hq.
 now apply IZR_le.
 rewrite <- plus_IZR.
 apply IZR_le.
-clear -Hr ; omega.
+clear -Hr ; lia.
 apply Rmult_le_pos.
 now apply IZR_le.
 apply sqrt_ge_0.
@@ -188,7 +189,7 @@ set (e := Z.min _ _).
 assert (2 * e <= e1)%Z as He.
 { assert (e <= Z.div2 e1)%Z by apply Z.le_min_r.
   rewrite (Zdiv2_odd_eqn e1).
-  destruct Z.odd ; omega. }
+  destruct Z.odd ; lia. }
 generalize (Fsqrt_core_correct m1 e1 e Hm1 He).
 destruct Fsqrt_core as [m l].
 apply conj.
diff --git a/flocq/Core/Defs.v b/flocq/Core/Defs.v
index f5c6f33b..27342df9 100644
--- a/flocq/Core/Defs.v
+++ b/flocq/Core/Defs.v
@@ -80,4 +80,8 @@ Definition Rnd_NA_pt (F : R -> Prop) (x f : R) :=
   Rnd_N_pt F x f /\
   forall f2 : R, Rnd_N_pt F x f2 -> (Rabs f2 <= Rabs f)%R.
 
+Definition Rnd_N0_pt (F : R -> Prop) (x f : R) :=
+  Rnd_N_pt F x f /\
+  forall f2 : R, Rnd_N_pt F x f2 -> (Rabs f <= Rabs f2)%R.
+
 End RND.
diff --git a/flocq/Core/Digits.v b/flocq/Core/Digits.v
index bed2e20a..a18ff8d6 100644
--- a/flocq/Core/Digits.v
+++ b/flocq/Core/Digits.v
@@ -17,8 +17,13 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 COPYING file for more details.
 *)
 
-Require Import ZArith Zquot.
+From Coq Require Import Lia ZArith Zquot.
+
 Require Import Zaux.
+Require Import SpecFloatCompat.
+
+Notation digits2_pos := digits2_pos (only parsing).
+Notation Zdigits2 := Zdigits2 (only parsing).
 
 (** Number of bits (radix 2) of a positive integer.
 
@@ -41,9 +46,9 @@ intros n d. unfold d. clear.
 assert (Hp: forall m, (Zpower_nat 2 (S m) = 2 * Zpower_nat 2 m)%Z) by easy.
 induction n ; simpl digits2_Pnat.
 rewrite Zpos_xI, 2!Hp.
-omega.
+lia.
 rewrite (Zpos_xO n), 2!Hp.
-omega.
+lia.
 now split.
 Qed.
 
@@ -185,13 +190,13 @@ apply Zgt_not_eq.
 now apply Zpower_gt_0.
 now apply Zle_minus_le_0.
 destruct (Zle_or_lt 0 k) as [H0|H0].
-rewrite (Zdigit_lt n) by omega.
+rewrite (Zdigit_lt n) by lia.
 unfold Zdigit.
 replace k' with (k' - k + k)%Z by ring.
 rewrite Zpower_plus with (2 := H0).
 rewrite Zmult_assoc, Z_quot_mult.
 replace (k' - k)%Z with (k' - k - 1 + 1)%Z by ring.
-rewrite Zpower_exp by omega.
+rewrite Zpower_exp by lia.
 rewrite Zmult_assoc.
 change (Zpower beta 1) with (beta * 1)%Z.
 rewrite Zmult_1_r.
@@ -203,7 +208,7 @@ now apply Zlt_le_weak.
 rewrite Zdigit_lt with (1 := H0).
 apply sym_eq.
 apply Zdigit_lt.
-omega.
+lia.
 Qed.
 
 Theorem Zdigit_div_pow :
@@ -227,7 +232,7 @@ unfold Zdigit.
 rewrite <- 2!ZOdiv_mod_mult.
 apply (f_equal (fun x => Z.quot x (beta ^ k))).
 replace k' with (k + 1 + (k' - (k + 1)))%Z by ring.
-rewrite Zpower_exp by omega.
+rewrite Zpower_exp by lia.
 rewrite Zmult_comm.
 rewrite Zpower_plus by easy.
 change (Zpower beta 1) with (beta * 1)%Z.
@@ -449,7 +454,7 @@ unfold Zscale.
 case Zle_bool_spec ; intros Hk.
 now apply Zdigit_mul_pow.
 apply Zdigit_div_pow with (1 := Hk').
-omega.
+lia.
 Qed.
 
 Theorem Zscale_0 :
@@ -492,7 +497,7 @@ now rewrite Zpower_plus.
 now apply Zplus_le_0_compat.
 case Zle_bool_spec ; intros Hk''.
 pattern k at 1 ; replace k with (k + k' + -k')%Z by ring.
-assert (0 <= -k')%Z by omega.
+assert (0 <= -k')%Z by lia.
 rewrite Zpower_plus by easy.
 rewrite Zmult_assoc, Z_quot_mult.
 apply refl_equal.
@@ -503,7 +508,7 @@ rewrite Zpower_plus with (2 := Hk).
 apply Zquot_mult_cancel_r.
 apply Zgt_not_eq.
 now apply Zpower_gt_0.
-omega.
+lia.
 Qed.
 
 Theorem Zscale_scale :
@@ -532,7 +537,7 @@ rewrite Zdigit_mod_pow by apply Hk.
 rewrite Zdigit_scale by apply Hk.
 unfold Zminus.
 now rewrite Z.opp_involutive, Zplus_comm.
-omega.
+lia.
 Qed.
 
 Theorem Zdigit_slice_out :
@@ -589,16 +594,16 @@ destruct (Zle_or_lt k2' k) as [Hk''|Hk''].
 now apply Zdigit_slice_out.
 rewrite Zdigit_slice by now split.
 apply Zdigit_slice_out.
-zify ; omega.
-rewrite Zdigit_slice by (zify ; omega).
+zify ; lia.
+rewrite Zdigit_slice by (zify ; lia).
 rewrite (Zdigit_slice n (k1 + k1')) by now split.
 rewrite Zdigit_slice.
 now rewrite Zplus_assoc.
-zify ; omega.
+zify ; lia.
 unfold Zslice.
 rewrite Z.min_r.
 now rewrite Zle_bool_false.
-omega.
+lia.
 Qed.
 
 Theorem Zslice_mul_pow :
@@ -624,14 +629,14 @@ case Zle_bool_spec ; intros Hk2.
 apply (f_equal (fun x => Z.rem x (beta ^ k2))).
 unfold Zscale.
 case Zle_bool_spec ; intros Hk1'.
-replace k1 with Z0 by omega.
+replace k1 with Z0 by lia.
 case Zle_bool_spec ; intros Hk'.
-replace k with Z0 by omega.
+replace k with Z0 by lia.
 simpl.
 now rewrite Z.quot_1_r.
 rewrite Z.opp_involutive.
 apply Zmult_1_r.
-rewrite Zle_bool_false by omega.
+rewrite Zle_bool_false by lia.
 rewrite 2!Z.opp_involutive, Zplus_comm.
 rewrite Zpower_plus by assumption.
 apply Zquot_Zquot.
@@ -646,7 +651,7 @@ unfold Zscale.
 case Zle_bool_spec; intros Hk.
 now apply Zslice_mul_pow.
 apply Zslice_div_pow with (2 := Hk1).
-omega.
+lia.
 Qed.
 
 Theorem Zslice_div_pow_scale :
@@ -666,7 +671,7 @@ apply Zdigit_slice_out.
 now apply Zplus_le_compat_l.
 rewrite Zdigit_slice by now split.
 destruct (Zle_or_lt 0 (k1 + k')) as [Hk1'|Hk1'].
-rewrite Zdigit_slice by omega.
+rewrite Zdigit_slice by lia.
 rewrite Zdigit_div_pow by assumption.
 apply f_equal.
 ring.
@@ -685,15 +690,15 @@ rewrite Zdigit_plus.
 rewrite Zdigit_scale with (1 := Hk).
 destruct (Zle_or_lt (l1 + l2) k) as [Hk2|Hk2].
 rewrite Zdigit_slice_out with (1 := Hk2).
-now rewrite 2!Zdigit_slice_out by omega.
+now rewrite 2!Zdigit_slice_out by lia.
 rewrite Zdigit_slice with (1 := conj Hk Hk2).
 destruct (Zle_or_lt l1 k) as [Hk1|Hk1].
 rewrite Zdigit_slice_out with (1 := Hk1).
-rewrite Zdigit_slice by omega.
+rewrite Zdigit_slice by lia.
 simpl ; apply f_equal.
 ring.
 rewrite Zdigit_slice with (1 := conj Hk Hk1).
-rewrite (Zdigit_lt _ (k - l1)) by omega.
+rewrite (Zdigit_lt _ (k - l1)) by lia.
 apply Zplus_0_r.
 rewrite Zmult_comm.
 apply Zsame_sign_trans_weak with n.
@@ -713,7 +718,7 @@ left.
 now apply Zdigit_slice_out.
 right.
 apply Zdigit_lt.
-omega.
+lia.
 Qed.
 
 Section digits_aux.
@@ -788,7 +793,7 @@ pattern (radix_val beta) at 2 5 ; replace (radix_val beta) with (Zpower beta 1)
 rewrite <- Zpower_plus.
 rewrite Zplus_comm.
 apply IHu.
-clear -Hv ; omega.
+clear -Hv ; lia.
 split.
 now ring_simplify (1 + v - 1)%Z.
 now rewrite Zplus_assoc.
@@ -928,7 +933,7 @@ intros x y Zx Hxy.
 assert (Hx := Zdigits_correct x).
 assert (Hy := Zdigits_correct y).
 apply (Zpower_lt_Zpower beta).
-zify ; omega.
+zify ; lia.
 Qed.
 
 Theorem lt_Zdigits :
@@ -938,7 +943,7 @@ Theorem lt_Zdigits :
   (x < y)%Z.
 Proof.
 intros x y Hy.
-cut (y <= x -> Zdigits y <= Zdigits x)%Z. omega.
+cut (y <= x -> Zdigits y <= Zdigits x)%Z. lia.
 now apply Zdigits_le.
 Qed.
 
@@ -951,7 +956,7 @@ intros e x Hex.
 destruct (Zdigits_correct x) as [H1 H2].
 apply Z.le_trans with (2 := H1).
 apply Zpower_le.
-clear -Hex ; omega.
+clear -Hex ; lia.
 Qed.
 
 Theorem Zdigits_le_Zpower :
@@ -961,7 +966,7 @@ Theorem Zdigits_le_Zpower :
 Proof.
 intros e x.
 generalize (Zpower_le_Zdigits e x).
-omega.
+lia.
 Qed.
 
 Theorem Zpower_gt_Zdigits :
@@ -982,7 +987,7 @@ Theorem Zdigits_gt_Zpower :
 Proof.
 intros e x Hex.
 generalize (Zpower_gt_Zdigits e x).
-omega.
+lia.
 Qed.
 
 (** Number of digits of a product.
@@ -1010,8 +1015,8 @@ apply Zdigits_correct.
 apply Zlt_le_succ.
 rewrite <- (Z.abs_eq y) at 1 by easy.
 apply Zdigits_correct.
-clear -Hx ; omega.
-clear -Hy ; omega.
+clear -Hx ; lia.
+clear -Hy ; lia.
 change Z0 with (0 + 0 + 0)%Z.
 apply Zplus_le_compat.
 now apply Zplus_le_compat.
@@ -1031,7 +1036,7 @@ apply Zdigits_le.
 apply Zabs_pos.
 rewrite Zabs_Zmult.
 generalize (Zabs_pos x) (Zabs_pos y).
-omega.
+lia.
 apply Zdigits_mult_strong ; apply Zabs_pos.
 Qed.
 
@@ -1041,7 +1046,7 @@ Theorem Zdigits_mult_ge :
   (Zdigits x + Zdigits y - 1 <= Zdigits (x * y))%Z.
 Proof.
 intros x y Zx Zy.
-cut ((Zdigits x - 1) + (Zdigits y - 1) < Zdigits (x * y))%Z. omega.
+cut ((Zdigits x - 1) + (Zdigits y - 1) < Zdigits (x * y))%Z. lia.
 apply Zdigits_gt_Zpower.
 rewrite Zabs_Zmult.
 rewrite Zpower_exp.
@@ -1052,8 +1057,8 @@ apply Zpower_le_Zdigits.
 apply Zlt_pred.
 apply Zpower_ge_0.
 apply Zpower_ge_0.
-generalize (Zdigits_gt_0 x). omega.
-generalize (Zdigits_gt_0 y). omega.
+generalize (Zdigits_gt_0 x). lia.
+generalize (Zdigits_gt_0 y). lia.
 Qed.
 
 Theorem Zdigits_div_Zpower :
@@ -1073,7 +1078,7 @@ destruct (Zle_lt_or_eq _ _ (proj2 He)) as [He'|He'].
   replace (Zdigits m - e - 1)%Z with (Zdigits m - 1 - e)%Z by ring.
   rewrite Z.pow_sub_r.
   2: apply Zgt_not_eq, radix_gt_0.
-  2: clear -He He' ; omega.
+  2: clear -He He' ; lia.
   apply Z_div_le with (2 := H1).
   now apply Z.lt_gt, Zpower_gt_0.
   apply Zmult_lt_reg_r with (Zpower beta e).
@@ -1118,13 +1123,6 @@ rewrite <- Zpower_nat_Z.
 apply digits2_Pnat_correct.
 Qed.
 
-Fixpoint digits2_pos (n : positive) : positive :=
-  match n with
-  | xH => xH
-  | xO p => Pos.succ (digits2_pos p)
-  | xI p => Pos.succ (digits2_pos p)
-  end.
-
 Theorem Zpos_digits2_pos :
   forall m : positive,
   Zpos (digits2_pos m) = Zdigits radix2 (Zpos m).
@@ -1137,13 +1135,6 @@ induction m ; simpl ; try easy ;
   apply f_equal, IHm.
 Qed.
 
-Definition Zdigits2 n :=
-  match n with
-  | Z0 => n
-  | Zpos p => Zpos (digits2_pos p)
-  | Zneg p => Zpos (digits2_pos p)
-  end.
-
 Lemma Zdigits2_Zdigits :
   forall n, Zdigits2 n = Zdigits radix2 n.
 Proof.
diff --git a/flocq/Core/FIX.v b/flocq/Core/FIX.v
index 4e0a25e6..779d94cb 100644
--- a/flocq/Core/FIX.v
+++ b/flocq/Core/FIX.v
@@ -18,6 +18,8 @@ COPYING file for more details.
 *)
 
 (** * Fixed-point format *)
+
+From Coq Require Import Lia.
 Require Import Raux Defs Round_pred Generic_fmt Ulp Round_NE.
 
 Section RND_FIX.
@@ -86,9 +88,16 @@ intros x; unfold ulp.
 case Req_bool_spec; intros Zx.
 case (negligible_exp_spec FIX_exp).
 intros T; specialize (T (emin-1)%Z); contradict T.
-unfold FIX_exp; omega.
+unfold FIX_exp; lia.
 intros n _; reflexivity.
 reflexivity.
 Qed.
 
+Global Instance exists_NE_FIX :
+      Exists_NE beta FIX_exp.
+Proof.
+unfold Exists_NE, FIX_exp; simpl.
+right; split; auto.
+Qed.
+
 End RND_FIX.
diff --git a/flocq/Core/FLT.v b/flocq/Core/FLT.v
index bd48d4b7..7301328d 100644
--- a/flocq/Core/FLT.v
+++ b/flocq/Core/FLT.v
@@ -46,7 +46,7 @@ intros k.
 unfold FLT_exp.
 generalize (prec_gt_0 prec).
 repeat split ;
-  intros ; zify ; omega.
+  intros ; zify ; lia.
 Qed.
 
 Theorem generic_format_FLT :
@@ -93,24 +93,28 @@ simpl in ex.
 specialize (He Hx0).
 apply Rlt_le_trans with (1 := proj2 He).
 apply bpow_le.
-cut (ex' - prec <= ex)%Z. omega.
+cut (ex' - prec <= ex)%Z. lia.
 unfold ex, FLT_exp.
 apply Z.le_max_l.
 apply Z.le_max_r.
 Qed.
 
-
-Theorem FLT_format_bpow :
+Theorem generic_format_FLT_bpow :
   forall e, (emin <= e)%Z -> generic_format beta FLT_exp (bpow e).
 Proof.
 intros e He.
 apply generic_format_bpow; unfold FLT_exp.
 apply Z.max_case; try assumption.
-unfold Prec_gt_0 in prec_gt_0_; omega.
+unfold Prec_gt_0 in prec_gt_0_; lia.
 Qed.
 
-
-
+Theorem FLT_format_bpow :
+  forall e, (emin <= e)%Z -> FLT_format (bpow e).
+Proof.
+intros e He.
+apply FLT_format_generic.
+now apply generic_format_FLT_bpow.
+Qed.
 
 Theorem FLT_format_satisfies_any :
   satisfies_any FLT_format.
@@ -136,12 +140,40 @@ apply Zmax_left.
 destruct (mag beta x) as (ex, He).
 unfold FLX_exp. simpl.
 specialize (He Hx0).
-cut (emin + prec - 1 < ex)%Z. omega.
+cut (emin + prec - 1 < ex)%Z. lia.
 apply (lt_bpow beta).
 apply Rle_lt_trans with (1 := Hx).
 apply He.
 Qed.
 
+(** FLT is a nice format: it has a monotone exponent... *)
+Global Instance FLT_exp_monotone : Monotone_exp FLT_exp.
+Proof.
+intros ex ey.
+unfold FLT_exp.
+zify ; lia.
+Qed.
+
+(** and it allows a rounding to nearest, ties to even. *)
+Global Instance exists_NE_FLT :
+  (Z.even beta = false \/ (1 < prec)%Z) ->
+  Exists_NE beta FLT_exp.
+Proof.
+intros [H|H].
+now left.
+right.
+intros e.
+unfold FLT_exp.
+destruct (Zmax_spec (e - prec) emin) as [(H1,H2)|(H1,H2)] ;
+  rewrite H2 ; clear H2.
+generalize (Zmax_spec (e + 1 - prec) emin).
+generalize (Zmax_spec (e - prec + 1 - prec) emin).
+lia.
+generalize (Zmax_spec (e + 1 - prec) emin).
+generalize (Zmax_spec (emin + 1 - prec) emin).
+lia.
+Qed.
+
 (** Links between FLT and FLX *)
 Theorem generic_format_FLT_FLX :
   forall x : R,
@@ -192,7 +224,7 @@ apply Zmax_right.
 unfold FIX_exp.
 destruct (mag beta x) as (ex, Hex).
 simpl.
-cut (ex - 1 < emin + prec)%Z. omega.
+cut (ex - 1 < emin + prec)%Z. lia.
 apply (lt_bpow beta).
 apply Rle_lt_trans with (2 := Hx).
 now apply Hex.
@@ -222,7 +254,7 @@ apply generic_inclusion_le...
 intros e He.
 unfold FIX_exp.
 apply Z.max_lub.
-omega.
+lia.
 apply Z.le_refl.
 Qed.
 
@@ -238,45 +270,53 @@ destruct (Z.max_spec (n - prec) emin) as [(Hm, Hm')|(Hm, Hm')].
 revert Hn prec_gt_0_; unfold FLT_exp, Prec_gt_0; rewrite Hm'; lia.
 Qed.
 
-Theorem generic_format_FLT_1 (Hemin : (emin <= 0)%Z) :
+Theorem generic_format_FLT_1 :
+  (emin <= 0)%Z ->
   generic_format beta FLT_exp 1.
 Proof.
-unfold generic_format, scaled_mantissa, cexp, F2R; simpl.
-rewrite Rmult_1_l, (mag_unique beta 1 1).
-{ unfold FLT_exp.
-  destruct (Z.max_spec_le (1 - prec) emin) as [(H,Hm)|(H,Hm)]; rewrite Hm;
-    (rewrite <- IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; omega]);
-    (rewrite Ztrunc_IZR, IZR_Zpower, <-bpow_plus;
-     [|unfold Prec_gt_0 in prec_gt_0_; omega]);
-    now replace (_ + _)%Z with Z0 by ring. }
-rewrite Rabs_R1; simpl; split; [now right|].
-rewrite IZR_Zpower_pos; simpl; rewrite Rmult_1_r; apply IZR_lt.
-apply (Z.lt_le_trans _ 2); [omega|]; apply Zle_bool_imp_le, beta.
+intros Hemin.
+now apply (generic_format_FLT_bpow 0).
 Qed.
 
-Theorem ulp_FLT_small: forall x, (Rabs x < bpow (emin+prec))%R ->
-    ulp beta FLT_exp x = bpow emin.
-Proof with auto with typeclass_instances.
+Theorem ulp_FLT_0 :
+  ulp beta FLT_exp 0 = bpow emin.
+Proof.
+unfold ulp.
+rewrite Req_bool_true by easy.
+case negligible_exp_spec.
+- intros T.
+  elim Zle_not_lt with (2 := T emin).
+  apply Z.le_max_r.
+- intros n Hn.
+  apply f_equal.
+  assert (H: FLT_exp emin = emin).
+    apply Z.max_r.
+    generalize (prec_gt_0 prec).
+    clear ; lia.
+  rewrite <- H.
+  apply fexp_negligible_exp_eq.
+  apply FLT_exp_valid.
+  exact Hn.
+  rewrite H.
+  apply Z.le_refl.
+Qed.
+
+Theorem ulp_FLT_small :
+  forall x, (Rabs x < bpow (emin + prec))%R ->
+  ulp beta FLT_exp x = bpow emin.
+Proof.
 intros x Hx.
-unfold ulp; case Req_bool_spec; intros Hx2.
-(* x = 0 *)
-case (negligible_exp_spec FLT_exp).
-intros T; specialize (T (emin-1)%Z); contradict T.
-apply Zle_not_lt; unfold FLT_exp.
-apply Z.le_trans with (2:=Z.le_max_r _ _); omega.
-assert (V:FLT_exp emin = emin).
-unfold FLT_exp; apply Z.max_r.
-unfold Prec_gt_0 in prec_gt_0_; omega.
-intros n H2; rewrite <-V.
-apply f_equal, fexp_negligible_exp_eq...
-omega.
-(* x <> 0 *)
-apply f_equal; unfold cexp, FLT_exp.
+destruct (Req_dec x 0%R) as [Zx|Zx].
+{ rewrite Zx.
+  apply ulp_FLT_0. }
+rewrite ulp_neq_0 by easy.
+apply f_equal.
 apply Z.max_r.
-assert (mag beta x-1 < emin+prec)%Z;[idtac|omega].
-destruct (mag beta x) as (e,He); simpl.
+destruct (mag beta x) as [e He].
+simpl.
+cut (e - 1 < emin + prec)%Z. lia.
 apply lt_bpow with beta.
-apply Rle_lt_trans with (2:=Hx).
+apply Rle_lt_trans with (2 := Hx).
 now apply He.
 Qed.
 
@@ -295,8 +335,8 @@ apply Rle_trans with (bpow (e-1)*bpow (1-prec))%R.
 rewrite <- bpow_plus.
 right; apply f_equal.
 replace (e - 1 + (1 - prec))%Z with (e - prec)%Z by ring.
-apply Z.max_l.
-assert (emin+prec-1 < e)%Z; try omega.
+apply Z.max_l; simpl.
+assert (emin+prec-1 < e)%Z; try lia.
 apply lt_bpow with beta.
 apply Rle_lt_trans with (1:=Hx).
 now apply He.
@@ -334,7 +374,7 @@ unfold ulp; rewrite Req_bool_false;
   [|now intro H; apply Nzx, (Rmult_eq_reg_r (bpow e));
     [rewrite Rmult_0_l|apply Rgt_not_eq, Rlt_gt, bpow_gt_0]].
 rewrite (Req_bool_false _ _ Nzx), <- bpow_plus; f_equal; unfold cexp, FLT_exp.
-rewrite (mag_mult_bpow _ _ _ Nzx), !Z.max_l; omega.
+rewrite (mag_mult_bpow _ _ _ Nzx), !Z.max_l; lia.
 Qed.
 
 Lemma succ_FLT_exact_shift_pos :
@@ -375,32 +415,106 @@ fold (Req_bool (-x) (bpow (mag beta (-x) - 1))); case Req_bool.
 rewrite ulp_FLT_exact_shift; [ring|lra| |]; rewrite mag_opp; lia.
 Qed.
 
-(** FLT is a nice format: it has a monotone exponent... *)
-Global Instance FLT_exp_monotone : Monotone_exp FLT_exp.
-Proof.
-intros ex ey.
-unfold FLT_exp.
-zify ; omega.
-Qed.
-
-(** and it allows a rounding to nearest, ties to even. *)
-Hypothesis NE_prop : Z.even beta = false \/ (1 < prec)%Z.
-
-Global Instance exists_NE_FLT : Exists_NE beta FLT_exp.
+Theorem ulp_FLT_pred_pos :
+  forall x,
+  generic_format beta FLT_exp x ->
+  (0 <= x)%R ->
+  ulp beta FLT_exp (pred beta FLT_exp x) = ulp beta FLT_exp x \/
+  (x = bpow (mag beta x - 1) /\ ulp beta FLT_exp (pred beta FLT_exp x) = (ulp beta FLT_exp x / IZR beta)%R).
 Proof.
-destruct NE_prop as [H|H].
-now left.
-right.
-intros e.
-unfold FLT_exp.
-destruct (Zmax_spec (e - prec) emin) as [(H1,H2)|(H1,H2)] ;
-  rewrite H2 ; clear H2.
-generalize (Zmax_spec (e + 1 - prec) emin).
-generalize (Zmax_spec (e - prec + 1 - prec) emin).
-omega.
-generalize (Zmax_spec (e + 1 - prec) emin).
-generalize (Zmax_spec (emin + 1 - prec) emin).
-omega.
+intros x Fx [Hx|Hx] ; cycle 1.
+{ rewrite <- Hx.
+  rewrite pred_0.
+  rewrite ulp_opp.
+  left.
+  apply ulp_ulp_0.
+  apply FLT_exp_valid.
+  typeclasses eauto. }
+assert (Hp: (0 <= pred beta FLT_exp x)%R).
+{ apply pred_ge_gt ; try easy.
+  apply FLT_exp_valid.
+  apply generic_format_0. }
+destruct (Rle_or_lt (bpow (emin + prec)) x) as [Hs|Hs].
+- unfold ulp.
+  rewrite Req_bool_false ; cycle 1.
+  { intros Zp.
+    apply Rle_not_lt with (1 := Hs).
+    generalize (f_equal (succ beta FLT_exp) Zp).
+    rewrite succ_pred.
+    rewrite succ_0, ulp_FLT_0.
+    intros H.
+    rewrite H.
+    apply bpow_lt.
+    generalize (prec_gt_0 prec).
+    lia.
+    apply FLT_exp_valid.
+    exact Fx. }
+  rewrite Req_bool_false by now apply Rgt_not_eq.
+  unfold cexp.
+  destruct (mag beta x) as [e He].
+  simpl.
+  specialize (He (Rgt_not_eq _ _ Hx)).
+  rewrite Rabs_pos_eq in He by now apply Rlt_le.
+  destruct (proj1 He) as [Hb|Hb].
+  + left.
+    apply (f_equal (fun v => bpow (FLT_exp v))).
+    apply mag_unique.
+    rewrite Rabs_pos_eq by easy.
+    split.
+    * apply pred_ge_gt ; try easy.
+      apply FLT_exp_valid.
+      apply generic_format_FLT_bpow.
+      apply Z.lt_le_pred.
+      apply lt_bpow with beta.
+      apply Rle_lt_trans with (2 := proj2 He).
+      apply Rle_trans with (2 := Hs).
+      apply bpow_le.
+      generalize (prec_gt_0 prec).
+      lia.
+    * apply pred_lt_le.
+      now apply Rgt_not_eq.
+      now apply Rlt_le.
+  + right.
+    split.
+    easy.
+    replace (FLT_exp _) with (FLT_exp e + -1)%Z.
+    rewrite bpow_plus.
+    now rewrite <- (Zmult_1_r beta).
+    rewrite <- Hb.
+    unfold FLT_exp at 1 2.
+    replace (mag_val _ _ (mag _ _)) with (e - 1)%Z.
+    rewrite <- Hb in Hs.
+    apply le_bpow in Hs.
+    zify ; lia.
+    apply eq_sym, mag_unique.
+    rewrite Hb.
+    rewrite Rabs_pos_eq by easy.
+    split ; cycle 1.
+    { apply pred_lt_id.
+      now apply Rgt_not_eq. }
+    apply pred_ge_gt.
+    apply FLT_exp_valid.
+    apply generic_format_FLT_bpow.
+    cut (emin + 1 < e)%Z. lia.
+    apply lt_bpow with beta.
+    apply Rle_lt_trans with (2 := proj2 He).
+    apply Rle_trans with (2 := Hs).
+    apply bpow_le.
+    generalize (prec_gt_0 prec).
+    lia.
+    exact Fx.
+    apply Rlt_le_trans with (2 := proj1 He).
+    apply bpow_lt.
+    apply Z.lt_pred_l.
+- left.
+  rewrite (ulp_FLT_small x).
+  apply ulp_FLT_small.
+  rewrite Rabs_pos_eq by easy.
+  apply pred_lt_le.
+  now apply Rgt_not_eq.
+  now apply Rlt_le.
+  rewrite Rabs_pos_eq by now apply Rlt_le.
+  exact Hs.
 Qed.
 
 End RND_FLT.
diff --git a/flocq/Core/FLX.v b/flocq/Core/FLX.v
index 803d96ef..78bffba5 100644
--- a/flocq/Core/FLX.v
+++ b/flocq/Core/FLX.v
@@ -48,7 +48,7 @@ Proof.
 intros k.
 unfold FLX_exp.
 generalize prec_gt_0.
-repeat split ; intros ; omega.
+repeat split ; intros ; lia.
 Qed.
 
 Theorem FIX_format_FLX :
@@ -212,7 +212,7 @@ Proof.
 case (negligible_exp_spec FLX_exp).
 intros _; reflexivity.
 intros n H2; contradict H2.
-unfold FLX_exp; unfold Prec_gt_0 in prec_gt_0_; omega.
+unfold FLX_exp; unfold Prec_gt_0 in prec_gt_0_; lia.
 Qed.
 
 Theorem generic_format_FLX_1 :
@@ -221,13 +221,13 @@ Proof.
 unfold generic_format, scaled_mantissa, cexp, F2R; simpl.
 rewrite Rmult_1_l, (mag_unique beta 1 1).
 { unfold FLX_exp.
-  rewrite <- IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; omega].
-  rewrite Ztrunc_IZR, IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; omega].
+  rewrite <- IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; lia].
+  rewrite Ztrunc_IZR, IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; lia].
   rewrite <- bpow_plus.
   now replace (_ + _)%Z with Z0 by ring. }
 rewrite Rabs_R1; simpl; split; [now right|].
 unfold Z.pow_pos; simpl; rewrite Zmult_1_r; apply IZR_lt.
-assert (H := Zle_bool_imp_le _ _ (radix_prop beta)); omega.
+assert (H := Zle_bool_imp_le _ _ (radix_prop beta)); lia.
 Qed.
 
 Theorem ulp_FLX_0: (ulp beta FLX_exp 0 = 0)%R.
@@ -356,7 +356,7 @@ destruct NE_prop as [H|H].
 now left.
 right.
 unfold FLX_exp.
-split ; omega.
+split ; lia.
 Qed.
 
 End RND_FLX.
diff --git a/flocq/Core/FTZ.v b/flocq/Core/FTZ.v
index 1a93bcd9..d6bae6ea 100644
--- a/flocq/Core/FTZ.v
+++ b/flocq/Core/FTZ.v
@@ -18,6 +18,8 @@ COPYING file for more details.
 *)
 
 (** * Floating-point format with abrupt underflow *)
+
+From Coq Require Import Lia.
 Require Import Raux Defs Round_pred Generic_fmt.
 Require Import Float_prop Ulp FLX.
 
@@ -48,22 +50,22 @@ unfold FTZ_exp.
 generalize (Zlt_cases (k - prec) emin).
 case (Zlt_bool (k - prec) emin) ; intros H1.
 split ; intros H2.
-omega.
+lia.
 split.
 generalize (Zlt_cases (emin + prec + 1 - prec) emin).
 case (Zlt_bool (emin + prec + 1 - prec) emin) ; intros H3.
-omega.
+lia.
 generalize (Zlt_cases (emin + prec - 1 + 1 - prec) emin).
 generalize (prec_gt_0 prec).
-case (Zlt_bool (emin + prec - 1 + 1 - prec) emin) ; omega.
+case (Zlt_bool (emin + prec - 1 + 1 - prec) emin) ; lia.
 intros l H3.
 generalize (Zlt_cases (l - prec) emin).
-case (Zlt_bool (l - prec) emin) ; omega.
+case (Zlt_bool (l - prec) emin) ; lia.
 split ; intros H2.
 generalize (Zlt_cases (k + 1 - prec) emin).
-case (Zlt_bool (k + 1 - prec) emin) ; omega.
+case (Zlt_bool (k + 1 - prec) emin) ; lia.
 generalize (prec_gt_0 prec).
-split ; intros ; omega.
+split ; intros ; lia.
 Qed.
 
 Theorem FLXN_format_FTZ :
@@ -94,7 +96,7 @@ rewrite Zlt_bool_false.
 apply Z.le_refl.
 rewrite Hx1, mag_F2R with (1 := Zxm).
 cut (prec - 1 < mag beta (IZR xm))%Z.
-clear -Hx3 ; omega.
+clear -Hx3 ; lia.
 apply mag_gt_Zpower with (1 := Zxm).
 apply Hx2.
 apply generic_format_FLXN.
@@ -135,7 +137,7 @@ change (0 < F2R (Float beta (Z.abs (Ztrunc (x * bpow (- (emin + prec - 1))))) (e
 rewrite F2R_Zabs, <- Hx2.
 now apply Rabs_pos_lt.
 apply bpow_le.
-omega.
+lia.
 rewrite Hx2.
 eexists ; repeat split ; simpl.
 apply le_IZR.
@@ -186,7 +188,7 @@ intros e He.
 unfold FTZ_exp.
 rewrite Zlt_bool_false.
 apply Z.le_refl.
-omega.
+lia.
 Qed.
 
 Theorem ulp_FTZ_0 :
@@ -196,12 +198,12 @@ unfold ulp; rewrite Req_bool_true; trivial.
 case (negligible_exp_spec FTZ_exp).
 intros T; specialize (T (emin-1)%Z); contradict T.
 apply Zle_not_lt; unfold FTZ_exp; unfold Prec_gt_0 in prec_gt_0_.
-rewrite Zlt_bool_true; omega.
+rewrite Zlt_bool_true; lia.
 assert (V:(FTZ_exp (emin+prec-1) = emin+prec-1)%Z).
-unfold FTZ_exp; rewrite Zlt_bool_true; omega.
+unfold FTZ_exp; rewrite Zlt_bool_true; lia.
 intros n H2; rewrite <-V.
 apply f_equal, fexp_negligible_exp_eq...
-omega.
+lia.
 Qed.
 
 
@@ -290,12 +292,12 @@ apply Rle_trans with (2 := proj1 He).
 apply bpow_le.
 unfold FLX_exp.
 generalize (prec_gt_0 prec).
-clear -He' ; omega.
+clear -He' ; lia.
 apply bpow_ge_0.
 unfold FLX_exp, FTZ_exp.
 rewrite Zlt_bool_false.
 apply refl_equal.
-clear -He' ; omega.
+clear -He' ; lia.
 Qed.
 
 Theorem round_FTZ_small :
@@ -331,7 +333,7 @@ intros He'.
 elim Rlt_not_le with (1 := Hx).
 apply Rle_trans with (2 := proj1 He).
 apply bpow_le.
-omega.
+lia.
 apply bpow_ge_0.
 Qed.
 
diff --git a/flocq/Core/Float_prop.v b/flocq/Core/Float_prop.v
index 804dd397..a1f48d04 100644
--- a/flocq/Core/Float_prop.v
+++ b/flocq/Core/Float_prop.v
@@ -18,6 +18,8 @@ COPYING file for more details.
 *)
 
 (** * Basic properties of floating-point formats: lemmas about mantissa, exponent... *)
+
+From Coq Require Import Lia.
 Require Import Raux Defs Digits.
 
 Section Float_prop.
@@ -360,7 +362,7 @@ unfold F2R. simpl.
 apply Rmult_le_compat_r.
 apply bpow_ge_0.
 apply IZR_le.
-omega.
+lia.
 Qed.
 
 Theorem F2R_lt_bpow :
@@ -379,7 +381,7 @@ rewrite <-IZR_Zpower. 2: now apply Zle_left.
 now apply IZR_lt.
 elim Zlt_not_le with (1 := Hm).
 simpl.
-cut (e' - e < 0)%Z. 2: omega.
+cut (e' - e < 0)%Z. 2: lia.
 clear.
 case (e' - e)%Z ; try easy.
 intros p _.
@@ -413,7 +415,7 @@ now elim (Zle_not_lt _ _ (Zabs_pos m)).
 (* . *)
 replace (e - e' + p)%Z with (e - (e' - p))%Z by ring.
 apply F2R_change_exp.
-cut (e' - 1 < e + p)%Z. omega.
+cut (e' - 1 < e + p)%Z. lia.
 apply (lt_bpow beta).
 apply Rle_lt_trans with (1 := Hf).
 rewrite <- F2R_Zabs, Zplus_comm, bpow_plus.
@@ -472,10 +474,10 @@ assert (Hd := Zdigits_correct beta n).
 assert (Hd' := Zdigits_gt_0 beta n).
 apply Zle_antisym ; apply (bpow_lt_bpow beta).
 apply Rle_lt_trans with (2 := proj2 He).
-rewrite <- IZR_Zpower by omega.
+rewrite <- IZR_Zpower by lia.
 now apply IZR_le.
 apply Rle_lt_trans with (1 := proj1 He).
-rewrite <- IZR_Zpower by omega.
+rewrite <- IZR_Zpower by lia.
 now apply IZR_lt.
 Qed.
 
diff --git a/flocq/Core/Generic_fmt.v b/flocq/Core/Generic_fmt.v
index cb37bd91..af1bf3c1 100644
--- a/flocq/Core/Generic_fmt.v
+++ b/flocq/Core/Generic_fmt.v
@@ -18,6 +18,8 @@ COPYING file for more details.
 *)
 
 (** * What is a real number belonging to a format, and many properties. *)
+
+From Coq Require Import Lia.
 Require Import Raux Defs Round_pred Float_prop.
 
 Section Generic.
@@ -52,7 +54,7 @@ apply Znot_ge_lt.
 intros Hl.
 apply Z.ge_le in Hl.
 assert (H' := proj2 (proj2 (valid_exp l) Hl) k).
-omega.
+lia.
 Qed.
 
 Theorem valid_exp_large' :
@@ -67,7 +69,7 @@ apply Z.ge_le in H'.
 assert (Hl := Z.le_trans _ _ _ H H').
 apply valid_exp in Hl.
 assert (H1 := proj2 Hl k H').
-omega.
+lia.
 Qed.
 
 Definition cexp x :=
@@ -425,7 +427,7 @@ rewrite Gx.
 replace (Ztrunc (scaled_mantissa x)) with Z0.
 apply F2R_0.
 cut (Z.abs (Ztrunc (scaled_mantissa x)) < 1)%Z.
-clear ; zify ; omega.
+clear ; zify ; lia.
 apply lt_IZR.
 rewrite abs_IZR.
 now rewrite <- scaled_mantissa_generic.
@@ -522,7 +524,7 @@ specialize (Ex Hxz).
 apply Rlt_le_trans with (1 := proj2 Ex).
 apply bpow_le.
 specialize (Hp ex).
-omega.
+lia.
 Qed.
 
 Theorem generic_format_bpow_inv' :
@@ -544,7 +546,7 @@ apply bpow_gt_0.
 split.
 apply bpow_ge_0.
 apply (bpow_lt _ _ 0).
-clear -He ; omega.
+clear -He ; lia.
 Qed.
 
 Theorem generic_format_bpow_inv :
@@ -555,7 +557,7 @@ Proof.
 intros e He.
 apply generic_format_bpow_inv' in He.
 assert (H := valid_exp_large' (e + 1) e).
-omega.
+lia.
 Qed.
 
 Section Fcore_generic_round_pos.
@@ -587,7 +589,7 @@ rewrite <- (Zrnd_IZR (Zceil x)).
 apply Zrnd_le.
 apply Zceil_ub.
 rewrite Zceil_floor_neq.
-omega.
+lia.
 intros H.
 rewrite <- H in Hx.
 rewrite Zfloor_IZR, Zrnd_IZR in Hx.
@@ -630,7 +632,7 @@ apply Rmult_le_compat_r.
 apply bpow_ge_0.
 assert (Hf: IZR (Zpower beta (ex - 1 - fexp ex)) = bpow (ex - 1 + - fexp ex)).
 apply IZR_Zpower.
-omega.
+lia.
 rewrite <- Hf.
 apply IZR_le.
 apply Zfloor_lub.
@@ -657,7 +659,7 @@ apply Rmult_le_compat_r.
 apply bpow_ge_0.
 assert (Hf: IZR (Zpower beta (ex - fexp ex)) = bpow (ex - fexp ex)).
 apply IZR_Zpower.
-omega.
+lia.
 rewrite <- Hf.
 apply IZR_le.
 apply Zceil_glb.
@@ -738,7 +740,7 @@ destruct (Zle_or_lt ex (fexp ex)) as [Hx1|Hx1].
   apply bpow_le.
   apply valid_exp, proj2 in Hx1.
   specialize (Hx1 ey).
-  omega.
+  lia.
 apply Rle_trans with (bpow ex).
 now apply round_bounded_large_pos.
 apply bpow_le.
@@ -1380,7 +1382,7 @@ specialize (He (Rgt_not_eq _ _ Hx)).
 rewrite Rabs_pos_eq in He. 2: now apply Rlt_le.
 apply Rle_trans with (bpow (ex - 1)).
 apply bpow_le.
-cut (e < ex)%Z. omega.
+cut (e < ex)%Z. lia.
 apply (lt_bpow beta).
 now apply Rle_lt_trans with (2 := proj2 He).
 destruct (Zle_or_lt ex (fexp ex)).
@@ -1389,7 +1391,7 @@ rewrite Hr in Hd.
 elim Rlt_irrefl with (1 := Hd).
 rewrite Hr.
 apply bpow_le.
-omega.
+lia.
 apply (round_bounded_large_pos rnd x ex H He).
 Qed.
 
@@ -1526,7 +1528,7 @@ unfold cexp.
 set (ex := mag beta x).
 generalize (exp_not_FTZ ex).
 generalize (proj2 (proj2 (valid_exp _) He) (fexp ex + 1)%Z).
-omega.
+lia.
 rewrite <- H.
 rewrite <- mult_IZR, Ztrunc_IZR.
 unfold F2R. simpl.
@@ -1802,7 +1804,7 @@ Theorem Znearest_imp :
 Proof.
 intros x n Hd.
 cut (Z.abs (Znearest x - n) < 1)%Z.
-clear ; zify ; omega.
+clear ; zify ; lia.
 apply lt_IZR.
 rewrite abs_IZR, minus_IZR.
 replace (IZR (Znearest x) - IZR n)%R with (- (x - IZR (Znearest x)) + (x - IZR n))%R by ring.
@@ -1937,7 +1939,7 @@ replace (- _ + _)%Z with 0%Z by ring; simpl; rewrite Rmult_1_r.
 apply (Rlt_le_trans _ _ _ (proj2 Hex)).
 apply Rle_trans with (bpow (fexp (mag beta x) - 1)).
 - apply bpow_le.
-  rewrite (mag_unique beta x ex); [omega|].
+  rewrite (mag_unique beta x ex); [lia|].
   now rewrite Rabs_right.
 - unfold Zminus; rewrite bpow_plus.
   rewrite Rmult_comm.
@@ -2012,6 +2014,68 @@ Qed.
 
 End rndNA.
 
+Notation Znearest0 := (Znearest (fun x => (Zlt_bool x 0))).
+
+Section rndN0.
+
+Global Instance valid_rnd_N0 : Valid_rnd Znearest0 := valid_rnd_N _.
+
+Theorem round_N0_pt :
+  forall x,
+  Rnd_N0_pt generic_format x (round Znearest0 x).
+Proof.
+intros x.
+generalize (round_N_pt (fun t => Zlt_bool t 0) x).
+set (f := round (Znearest (fun t => Zlt_bool t 0)) x).
+intros Rxf.
+destruct (Req_dec (x - round Zfloor x) (round Zceil x - x)) as [Hm|Hm].
+(* *)
+apply Rnd_N0_pt_N.
+apply generic_format_0.
+exact Rxf.
+destruct (Rle_or_lt 0 x) as [Hx|Hx].
+(* . *)
+rewrite Rabs_pos_eq with (1 := Hx).
+rewrite Rabs_pos_eq.
+unfold f.
+rewrite round_N_middle with (1 := Hm).
+rewrite Zlt_bool_false.
+now apply round_DN_pt.
+apply Zfloor_lub.
+apply Rmult_le_pos with (1 := Hx).
+apply bpow_ge_0.
+apply Rnd_N_pt_ge_0 with (2 := Hx) (3 := Rxf).
+apply generic_format_0.
+(* . *)
+rewrite Rabs_left with (1 := Hx).
+rewrite Rabs_left1.
+apply Ropp_le_contravar.
+unfold f.
+rewrite round_N_middle with (1 := Hm).
+rewrite Zlt_bool_true.
+now apply round_UP_pt.
+apply lt_IZR.
+apply Rle_lt_trans with (scaled_mantissa x).
+apply Zfloor_lb.
+simpl.
+rewrite <- (Rmult_0_l (bpow (- (cexp x))%Z)%R).
+apply Rmult_lt_compat_r with (2 := Hx).
+apply bpow_gt_0.
+apply Rnd_N_pt_le_0 with (3 := Rxf).
+apply generic_format_0.
+now apply Rlt_le.
+(* *)
+split.
+apply Rxf.
+intros g Rxg.
+rewrite Rnd_N_pt_unique with (3 := Hm) (4 := Rxf) (5 := Rxg).
+apply Rle_refl.
+apply round_DN_pt; easy.
+apply round_UP_pt; easy.
+Qed.
+
+End rndN0.
+
 Section rndN_opp.
 
 Theorem Znearest_opp :
@@ -2055,6 +2119,31 @@ rewrite opp_IZR.
 now rewrite Ropp_mult_distr_l_reverse.
 Qed.
 
+Lemma round_N0_opp :
+  forall x,
+  (round Znearest0 (- x) = - round Znearest0 x)%R.
+Proof.
+intros x.
+rewrite round_N_opp.
+apply Ropp_eq_compat.
+apply round_ext.
+clear x; intro x.
+unfold Znearest.
+case_eq (Rcompare (x - IZR (Zfloor x)) (/ 2)); intro C;
+[|reflexivity|reflexivity].
+apply Rcompare_Eq_inv in C.
+assert (H : negb (- (Zfloor x + 1) <? 0)%Z = (Zfloor x <? 0)%Z);
+  [|now rewrite H].
+rewrite negb_Zlt_bool.
+case_eq (Zfloor x <? 0)%Z; intro C'.
+apply Zlt_is_lt_bool in C'.
+apply Zle_bool_true.
+lia.
+apply Z.ltb_ge in C'.
+apply Zle_bool_false.
+lia.
+Qed.
+
 End rndN_opp.
 
 Lemma round_N_small :
@@ -2293,10 +2382,10 @@ rewrite negb_Zle_bool.
 case_eq (0 <=? Zfloor x)%Z; intro C'.
 - apply Zle_bool_imp_le in C'.
   apply Zlt_bool_true.
-  omega.
+  lia.
 - rewrite Z.leb_gt in C'.
   apply Zlt_bool_false.
-  omega.
+  lia.
 Qed.
 
 End rndNA_opp.
diff --git a/flocq/Core/Raux.v b/flocq/Core/Raux.v
index 8273a55b..58d1a630 100644
--- a/flocq/Core/Raux.v
+++ b/flocq/Core/Raux.v
@@ -907,6 +907,18 @@ rewrite Ropp_involutive.
 apply Zfloor_lb.
 Qed.
 
+Theorem Zceil_lb :
+  forall x : R,
+  (IZR (Zceil x) < x + 1)%R.
+Proof.
+intros x.
+unfold Zceil.
+rewrite opp_IZR.
+rewrite <-(Ropp_involutive (x + 1)), Ropp_plus_distr.
+apply Ropp_lt_contravar, (Rplus_lt_reg_r 1); ring_simplify.
+apply Zfloor_ub.
+Qed.
+
 Theorem Zceil_glb :
   forall n x,
   (x <= IZR n)%R ->
@@ -1305,9 +1317,9 @@ rewrite Ropp_inv_permute with (1 := Zy').
 rewrite <- 2!opp_IZR.
 rewrite <- Zmod_opp_opp.
 apply H.
-clear -Hy. omega.
+clear -Hy. lia.
 apply H.
-clear -Zy Hy. omega.
+clear -Zy Hy. lia.
 (* *)
 split.
 pattern (IZR (x / y)) at 1 ; rewrite <- Rplus_0_r.
@@ -1454,7 +1466,7 @@ rewrite <- (Rmult_1_r (bpow e1)).
 rewrite bpow_plus.
 apply Rmult_lt_compat_l.
 apply bpow_gt_0.
-assert (0 < e2 - e1)%Z by omega.
+assert (0 < e2 - e1)%Z by lia.
 destruct (e2 - e1)%Z ; try discriminate H0.
 clear.
 rewrite <- IZR_Zpower by easy.
@@ -1756,7 +1768,7 @@ rewrite Rabs_right in Hex; [|now apply Rle_ge; apply Rlt_le].
 rewrite Rabs_right in Hey; [|now apply Rle_ge; apply Rlt_le].
 apply (Rlt_le_trans _ _ _ Hex).
 apply Rle_trans with (bpow (ey - 1)); [|exact Hey].
-now apply bpow_le; omega.
+now apply bpow_le; lia.
 Qed.
 
 Theorem mag_bpow :
@@ -1900,7 +1912,7 @@ apply bpow_le.
 now apply Zlt_le_weak.
 apply IZR_le.
 clear -Zm.
-zify ; omega.
+zify ; lia.
 Qed.
 
 Lemma mag_mult :
@@ -1999,7 +2011,7 @@ assert (Hbeta : (2 <= r)%Z).
 { destruct r as (beta_val,beta_prop).
   now apply Zle_bool_imp_le. }
 intros x y Px Py Hln.
-assert (Oxy : (y < x)%R); [apply lt_mag;[assumption|omega]|].
+assert (Oxy : (y < x)%R); [apply lt_mag;[assumption|lia]|].
 destruct (mag x) as (ex,Hex).
 destruct (mag y) as (ey,Hey).
 simpl in Hln |- *.
@@ -2096,7 +2108,7 @@ split.
   unfold Rsqr ; rewrite <- bpow_plus.
   apply bpow_le.
   generalize (Zdiv2_odd_eqn (e + 1)).
-  destruct Z.odd ; intros ; omega.
+  destruct Z.odd ; intros ; lia.
 - rewrite <- (Rabs_pos_eq (bpow _)) by apply bpow_ge_0.
   apply Rsqr_lt_abs_0.
   rewrite Rsqr_sqrt by now apply Rlt_le.
@@ -2104,7 +2116,7 @@ split.
   unfold Rsqr ; rewrite <- bpow_plus.
   apply bpow_le.
   generalize (Zdiv2_odd_eqn (e + 1)).
-  destruct Z.odd ; intros ; omega.
+  destruct Z.odd ; intros ; lia.
 Qed.
 
 Lemma mag_1 : mag 1 = 1%Z :> Z.
@@ -2324,7 +2336,7 @@ refine (Rle_not_lt _ _ (lub (/ (INR (S N) + 1))%R _) _).
   refine (H _ _ Py).
   apply INR_lt in Hy.
   clear -Hy HyN.
-  omega.
+  lia.
   now apply Rlt_le, Rinv_0_lt_compat.
 rewrite S_INR, HN.
 ring_simplify (IZR (up (/ l)) - 1 + 1)%R.
@@ -2369,7 +2381,7 @@ rewrite <- (Z.opp_involutive n).
 rewrite <- (Z.abs_neq n).
 rewrite <- Zabs2Nat.id_abs.
 apply K.
-omega.
+lia.
 Qed.
 
 
diff --git a/flocq/Core/Round_NE.v b/flocq/Core/Round_NE.v
index 20b60ef5..b7387a62 100644
--- a/flocq/Core/Round_NE.v
+++ b/flocq/Core/Round_NE.v
@@ -18,6 +18,8 @@ COPYING file for more details.
 *)
 
 (** * Rounding to nearest, ties to even: existence, unicity... *)
+
+From Coq Require Import Lia.
 Require Import Raux Defs Round_pred Generic_fmt Float_prop Ulp.
 
 Notation ZnearestE := (Znearest (fun x => negb (Z.even x))).
@@ -148,7 +150,7 @@ split.
 apply (round_DN_pt beta fexp x).
 apply generic_format_bpow.
 ring_simplify (ex - 1 + 1)%Z.
-omega.
+lia.
 apply Hex.
 apply Rle_lt_trans with (2 := proj2 Hex).
 apply (round_DN_pt beta fexp x).
@@ -209,14 +211,14 @@ rewrite Z.even_add.
 rewrite eqb_sym. simpl.
 fold (negb (Z.even (beta ^ (ex - fexp ex)))).
 rewrite Bool.negb_involutive.
-rewrite (Z.even_pow beta (ex - fexp ex)). 2: omega.
+rewrite (Z.even_pow beta (ex - fexp ex)) by lia.
 destruct exists_NE_.
 rewrite H.
 apply Zeven_Zpower_odd with (2 := H).
 now apply Zle_minus_le_0.
 apply Z.even_pow.
 specialize (H ex).
-omega.
+lia.
 (* - xu < bpow ex *)
 revert Hud.
 rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq].
@@ -413,18 +415,18 @@ now rewrite Hs in Hr.
 destruct (Hs ex) as (H,_).
 rewrite Z.even_pow.
 exact Hr.
-omega.
+lia.
 assert (Z.even (Zfloor mx) = true). 2: now rewrite H in Hmx.
-replace (Zfloor mx) with (Zceil mx + -1)%Z by omega.
+replace (Zfloor mx) with (Zceil mx + -1)%Z by lia.
 rewrite Z.even_add.
 apply eqb_true.
 unfold mx.
 replace (Zceil (scaled_mantissa beta fexp x)) with (Zpower beta (ex - fexp ex)).
 rewrite Zeven_Zpower_odd with (2 := Hr).
 easy.
-omega.
+lia.
 apply eq_IZR.
-rewrite IZR_Zpower. 2: omega.
+rewrite IZR_Zpower by lia.
 apply Rmult_eq_reg_r with (bpow (fexp ex)).
 unfold Zminus.
 rewrite bpow_plus.
@@ -434,7 +436,7 @@ now apply sym_eq.
 apply Rgt_not_eq.
 apply bpow_gt_0.
 generalize (proj1 (valid_exp ex) He).
-omega.
+lia.
 (* .. small pos *)
 assert (Z.even (Zfloor mx) = true). 2: now rewrite H in Hmx.
 unfold mx, scaled_mantissa.
diff --git a/flocq/Core/Round_pred.v b/flocq/Core/Round_pred.v
index 428a4bac..b7b6778f 100644
--- a/flocq/Core/Round_pred.v
+++ b/flocq/Core/Round_pred.v
@@ -42,6 +42,9 @@ Definition Rnd_NG (F : R -> Prop) (P : R -> R -> Prop) (rnd : R -> R) :=
 Definition Rnd_NA (F : R -> Prop) (rnd : R -> R) :=
   forall x : R, Rnd_NA_pt F x (rnd x).
 
+Definition Rnd_N0 (F : R -> Prop) (rnd : R -> R) :=
+  forall x : R, Rnd_N0_pt F x (rnd x).
+
 Theorem round_val_of_pred :
   forall rnd : R -> R -> Prop,
   round_pred rnd ->
@@ -1021,6 +1024,251 @@ intros F x f (Hf,_) Hx.
 now apply Rnd_N_pt_idempotent with F.
 Qed.
 
+Theorem Rnd_N0_NG_pt :
+  forall F : R -> Prop,
+  F 0 ->
+  forall x f,
+  Rnd_N0_pt F x f <-> Rnd_NG_pt F (fun x f => Rabs f <= Rabs x) x f.
+Proof.
+intros F HF x f.
+destruct (Rle_or_lt 0 x) as [Hx|Hx].
+(* *)
+split ; intros (H1, H2).
+(* . *)
+assert (Hf := Rnd_N_pt_ge_0 F HF x f Hx H1).
+split.
+exact H1.
+destruct (Rnd_N_pt_DN_or_UP _ _ _ H1) as [H3|H3].
+(* . . *)
+left.
+rewrite Rabs_pos_eq with (1 := Hf).
+rewrite Rabs_pos_eq with (1 := Hx).
+apply H3.
+(* . . *)
+right.
+intros f2 Hxf2.
+specialize (H2 _ Hxf2).
+destruct (Rnd_N_pt_DN_or_UP _ _ _ Hxf2) as [H4|H4].
+apply Rle_antisym.
+apply Rle_trans with x.
+apply H4.
+apply H3.
+rewrite Rabs_pos_eq with (1 := Hf) in H2.
+rewrite Rabs_pos_eq in H2.
+exact H2.
+now apply Rnd_N_pt_ge_0 with F x.
+eapply Rnd_UP_pt_unique ; eassumption.
+(* . *)
+split.
+exact H1.
+intros f2 Hxf2.
+destruct H2 as [H2|H2].
+assert (Hf := Rnd_N_pt_ge_0 F HF x f Hx H1).
+assert (Hf2 := Rnd_N_pt_ge_0 F HF x f2 Hx Hxf2).
+rewrite 2!Rabs_pos_eq ; trivial.
+rewrite 2!Rabs_pos_eq in H2 ; trivial.
+destruct (Rnd_N_pt_DN_or_UP _ _ _ Hxf2) as [H3|H3].
+apply H3.
+apply H1.
+apply H2.
+apply Rle_trans with (1 := H2).
+apply H3.
+rewrite (H2 _ Hxf2).
+apply Rle_refl.
+(* *)
+assert (Hx' := Rlt_le _ _ Hx).
+clear Hx. rename Hx' into Hx.
+split ; intros (H1, H2).
+(* . *)
+assert (Hf := Rnd_N_pt_le_0 F HF x f Hx H1).
+split.
+exact H1.
+destruct (Rnd_N_pt_DN_or_UP _ _ _ H1) as [H3|H3].
+(* . . *)
+right.
+intros f2 Hxf2.
+specialize (H2 _ Hxf2).
+destruct (Rnd_N_pt_DN_or_UP _ _ _ Hxf2) as [H4|H4].
+eapply Rnd_DN_pt_unique ; eassumption.
+apply Rle_antisym.
+2: apply Rle_trans with x.
+2: apply H3.
+2: apply H4.
+rewrite Rabs_left1 with (1 := Hf) in H2.
+rewrite Rabs_left1 in H2.
+now apply Ropp_le_cancel.
+now apply Rnd_N_pt_le_0 with F x.
+(* . . *)
+left.
+rewrite Rabs_left1 with (1 := Hf).
+rewrite Rabs_left1 with (1 := Hx).
+apply Ropp_le_contravar.
+apply H3.
+(* . *)
+split.
+exact H1.
+intros f2 Hxf2.
+destruct H2 as [H2|H2].
+assert (Hf := Rnd_N_pt_le_0 F HF x f Hx H1).
+assert (Hf2 := Rnd_N_pt_le_0 F HF x f2 Hx Hxf2).
+rewrite 2!Rabs_left1 ; trivial.
+rewrite 2!Rabs_left1 in H2 ; trivial.
+apply Ropp_le_contravar.
+apply Ropp_le_cancel in H2.
+destruct (Rnd_N_pt_DN_or_UP _ _ _ Hxf2) as [H3|H3].
+2: apply H3.
+2: apply H1.
+2: apply H2.
+apply Rle_trans with (2 := H2).
+apply H3.
+rewrite (H2 _ Hxf2).
+apply Rle_refl.
+Qed.
+
+Lemma Rnd_N0_pt_unique_prop :
+  forall F : R -> Prop,
+  F 0 ->
+  Rnd_NG_pt_unique_prop F (fun x f => Rabs f <= Rabs x).
+Proof.
+intros F HF x d u Hxd1 Hxd2 Hxu1 Hxu2 Hd Hu.
+apply Rle_antisym.
+apply Rle_trans with x.
+apply Hxd1.
+apply Hxu1.
+destruct (Rle_or_lt 0 x) as [Hx|Hx].
+apply Hxd1.
+apply Hxu1.
+rewrite Rabs_pos_eq with (1 := Hx) in Hu.
+rewrite Rabs_pos_eq in Hu.
+exact Hu.
+apply Rle_trans with (1:=Hx).
+apply Hxu1.
+(* *)
+apply Hxu1.
+apply Hxd1.
+rewrite Rabs_left with (1 := Hx) in Hd.
+rewrite Rabs_left1 in Hd.
+now apply Ropp_le_cancel.
+apply Rlt_le, Rle_lt_trans with (2:=Hx).
+apply Hxd1.
+Qed.
+
+Theorem Rnd_N0_pt_unique :
+  forall F : R -> Prop,
+  F 0 ->
+  forall x f1 f2 : R,
+  Rnd_N0_pt F x f1 -> Rnd_N0_pt F x f2 ->
+  f1 = f2.
+Proof.
+intros F HF x f1 f2 H1 H2.
+apply (Rnd_NG_pt_unique F _ (Rnd_N0_pt_unique_prop F HF) x).
+now apply -> Rnd_N0_NG_pt.
+now apply -> Rnd_N0_NG_pt.
+Qed.
+
+Theorem Rnd_N0_pt_N :
+  forall F : R -> Prop,
+  F 0 ->
+  forall x f : R,
+  Rnd_N_pt F x f ->
+  (Rabs f <= Rabs x)%R ->
+  Rnd_N0_pt F x f.
+Proof.
+intros F HF x f Rxf Hxf.
+split.
+apply Rxf.
+intros g Rxg.
+destruct (Rabs_eq_Rabs (f - x) (g - x)) as [H|H].
+apply Rle_antisym.
+apply Rxf.
+apply Rxg.
+apply Rxg.
+apply Rxf.
+(* *)
+replace g with f.
+apply Rle_refl.
+apply Rplus_eq_reg_r with (1 := H).
+(* *)
+assert (g = 2 * x - f)%R.
+replace (2 * x - f)%R with (x - (f - x))%R by ring.
+rewrite H.
+ring.
+destruct (Rle_lt_dec 0 x) as [Hx|Hx].
+(* . *)
+revert Hxf.
+rewrite Rabs_pos_eq with (1 := Hx).
+rewrite 2!Rabs_pos_eq ; try ( apply (Rnd_N_pt_ge_0 F HF x) ; assumption ).
+intros Hxf.
+rewrite H0.
+apply Rplus_le_reg_r with f.
+ring_simplify.
+apply Rmult_le_compat_l with (2 := Hxf).
+now apply IZR_le.
+(* . *)
+revert Hxf.
+apply Rlt_le in Hx.
+rewrite Rabs_left1 with (1 := Hx).
+rewrite 2!Rabs_left1 ; try ( apply (Rnd_N_pt_le_0 F HF x) ; assumption ).
+intros Hxf.
+rewrite H0.
+apply Ropp_le_contravar.
+apply Rplus_le_reg_r with f.
+ring_simplify.
+apply Rmult_le_compat_l.
+now apply IZR_le.
+now apply Ropp_le_cancel.
+Qed.
+
+Theorem Rnd_N0_unique :
+  forall (F : R -> Prop),
+  F 0 ->
+  forall rnd1 rnd2 : R -> R,
+  Rnd_N0 F rnd1 -> Rnd_N0 F rnd2 ->
+  forall x, rnd1 x = rnd2 x.
+Proof.
+intros F HF rnd1 rnd2 H1 H2 x.
+now apply Rnd_N0_pt_unique with F x.
+Qed.
+
+Theorem Rnd_N0_pt_monotone :
+  forall F : R -> Prop,
+  F 0 ->
+  round_pred_monotone (Rnd_N0_pt F).
+Proof.
+intros F HF x y f g Hxf Hyg Hxy.
+apply (Rnd_NG_pt_monotone F _ (Rnd_N0_pt_unique_prop F HF) x y).
+now apply -> Rnd_N0_NG_pt.
+now apply -> Rnd_N0_NG_pt.
+exact Hxy.
+Qed.
+
+Theorem Rnd_N0_pt_refl :
+  forall F : R -> Prop,
+  forall x : R, F x ->
+  Rnd_N0_pt F x x.
+Proof.
+intros F x Hx.
+split.
+now apply Rnd_N_pt_refl.
+intros f Hxf.
+apply Req_le.
+apply f_equal.
+now apply sym_eq, Rnd_N_pt_idempotent with (1 := Hxf).
+Qed.
+
+Theorem Rnd_N0_pt_idempotent :
+  forall F : R -> Prop,
+  forall x f : R,
+  Rnd_N0_pt F x f -> F x ->
+  f = x.
+Proof.
+intros F x f (Hf,_) Hx.
+now apply Rnd_N_pt_idempotent with F.
+Qed.
+
+
+
+
 Theorem round_pred_ge_0 :
   forall P : R -> R -> Prop,
   round_pred_monotone P ->
@@ -1405,4 +1653,38 @@ apply Rnd_NA_pt_monotone.
 apply Hany.
 Qed.
 
+Theorem satisfies_any_imp_N0 :
+  forall F : R -> Prop,
+  F 0 -> satisfies_any F ->
+  round_pred (Rnd_N0_pt F).
+Proof.
+intros F HF0 Hany.
+split.
+assert (H : round_pred_total (Rnd_NG_pt F (fun a b => (Rabs b <= Rabs a)%R))).
+apply satisfies_any_imp_NG.
+apply Hany.
+intros x d u Hf Hd Hu.
+destruct (Rle_lt_dec 0 x) as [Hx|Hx].
+right.
+rewrite Rabs_pos_eq with (1 := Hx).
+rewrite Rabs_pos_eq.
+apply Hd.
+apply Hd; try easy.
+left.
+rewrite Rabs_left with (1 := Hx).
+rewrite Rabs_left1.
+apply Ropp_le_contravar.
+apply Hu.
+apply Hu; try easy.
+now apply Rlt_le.
+intros x.
+destruct (H x) as (f, Hf).
+exists f.
+apply <- Rnd_N0_NG_pt.
+apply Hf.
+apply HF0.
+apply Rnd_N0_pt_monotone.
+apply HF0.
+Qed.
+
 End RND_prop.
diff --git a/flocq/Core/Ulp.v b/flocq/Core/Ulp.v
index 4f4a5674..c42b3e65 100644
--- a/flocq/Core/Ulp.v
+++ b/flocq/Core/Ulp.v
@@ -57,7 +57,7 @@ Proof.
 unfold negligible_exp; destruct LPO_Z as [(n,Hn)|Hn].
 now apply negligible_Some.
 apply negligible_None.
-intros n; specialize (Hn n); omega.
+intros n; specialize (Hn n); lia.
 Qed.
 
 Lemma negligible_exp_spec': (negligible_exp = None /\ forall n, (fexp n < n)%Z)
@@ -66,7 +66,7 @@ Proof.
 unfold negligible_exp; destruct LPO_Z as [(n,Hn)|Hn].
 right; simpl; exists n; now split.
 left; split; trivial.
-intros n; specialize (Hn n); omega.
+intros n; specialize (Hn n); lia.
 Qed.
 
 Context { valid_exp : Valid_exp fexp }.
@@ -75,8 +75,8 @@ Lemma fexp_negligible_exp_eq: forall n m, (n <= fexp n)%Z -> (m <= fexp m)%Z ->
 Proof.
 intros n m Hn Hm.
 case (Zle_or_lt n m); intros H.
-apply valid_exp; omega.
-apply sym_eq, valid_exp; omega.
+apply valid_exp; lia.
+apply sym_eq, valid_exp; lia.
 Qed.
 
 
@@ -198,6 +198,17 @@ rewrite V.
 apply generic_format_0.
 Qed.
 
+Theorem ulp_canonical :
+  forall m e,
+  m <> 0%Z ->
+  canonical beta fexp (Float beta m e) ->
+  ulp (F2R (Float beta m e)) = bpow e.
+Proof.
+intros m e Hm Hc.
+rewrite ulp_neq_0 by now apply F2R_neq_0.
+apply f_equal.
+now apply sym_eq.
+Qed.
 
 Theorem ulp_bpow :
   forall e, ulp (bpow e) = bpow (fexp (e + 1)).
@@ -216,7 +227,6 @@ apply bpow_ge_0.
 apply Rgt_not_eq, Rlt_gt, bpow_gt_0.
 Qed.
 
-
 Lemma generic_format_ulp_0 :
   F (ulp 0).
 Proof.
@@ -238,17 +248,17 @@ rewrite Req_bool_true; trivial.
 case negligible_exp_spec.
 intros H1 _.
 apply generic_format_bpow.
-specialize (H1 (e+1)%Z); omega.
+specialize (H1 (e+1)%Z); lia.
 intros n H1 H2.
 apply generic_format_bpow.
 case (Zle_or_lt (e+1) (fexp (e+1))); intros H4.
 absurd (e+1 <= e)%Z.
-omega.
+lia.
 apply Z.le_trans with (1:=H4).
 replace (fexp (e+1)) with (fexp n).
 now apply le_bpow with beta.
 now apply fexp_negligible_exp_eq.
-omega.
+lia.
 Qed.
 
 (** The three following properties are equivalent:
@@ -300,10 +310,10 @@ case (Zle_or_lt l (fexp l)); intros Hl.
 rewrite (fexp_negligible_exp_eq n l); trivial; apply Z.le_refl.
 case (Zle_or_lt (fexp n) (fexp l)); trivial; intros K.
 absurd (fexp n <= fexp l)%Z.
-omega.
+lia.
 apply Z.le_trans with (2:= H _).
 apply Zeq_le, sym_eq, valid_exp; trivial.
-omega.
+lia.
 Qed.
 
 Lemma not_FTZ_ulp_ge_ulp_0:
@@ -374,8 +384,6 @@ rewrite Hn1 in H; discriminate.
 now apply bpow_mag_le.
 Qed.
 
-
-
 (** Definition and properties of pred and succ *)
 
 Definition pred_pos x :=
@@ -432,6 +440,17 @@ unfold pred.
 now rewrite Ropp_involutive.
 Qed.
 
+Theorem pred_bpow :
+  forall e, pred (bpow e) = (bpow e - bpow (fexp e))%R.
+Proof.
+intros e.
+rewrite pred_eq_pos by apply bpow_ge_0.
+unfold pred_pos.
+rewrite mag_bpow.
+replace (e + 1 - 1)%Z with e by ring.
+now rewrite Req_bool_true.
+Qed.
+
 (** pred and succ are in the format *)
 
 (* cannont be x <> ulp 0, due to the counter-example 1-bit FP format fexp: e -> e-1 *)
@@ -450,7 +469,7 @@ apply gt_0_F2R with beta (cexp beta fexp x).
 rewrite <- Fx.
 apply Rle_lt_trans with (2:=Hx).
 apply bpow_ge_0.
-omega.
+lia.
 case (Zle_lt_or_eq _ _ H); intros Hm.
 (* *)
 pattern x at 1 ; rewrite Fx.
@@ -533,7 +552,7 @@ rewrite ulp_neq_0.
 intro H.
 assert (ex-1 < cexp beta fexp x  < ex)%Z.
 split ; apply (lt_bpow beta) ; rewrite <- H ; easy.
-clear -H0. omega.
+clear -H0. lia.
 now apply Rgt_not_eq.
 apply Ex'.
 apply Rle_lt_trans with (2 := proj2 Ex').
@@ -555,7 +574,7 @@ apply gt_0_F2R with beta (cexp beta fexp x).
 rewrite <- Fx.
 apply Rle_lt_trans with (2:=proj1 Ex').
 apply bpow_ge_0.
-omega.
+lia.
 now apply Rgt_not_eq.
 Qed.
 
@@ -579,7 +598,7 @@ rewrite minus_IZR, IZR_Zpower.
 rewrite Rmult_minus_distr_r, Rmult_1_l.
 rewrite <- bpow_plus.
 now replace (e - 1 - fexp (e - 1) + fexp (e - 1))%Z with (e-1)%Z by ring.
-omega.
+lia.
 rewrite H.
 apply generic_format_F2R.
 intros _.
@@ -592,7 +611,7 @@ split.
 apply Rplus_le_reg_l with (bpow (fexp (e-1))).
 ring_simplify.
 apply Rle_trans with (bpow (e - 2) + bpow (e - 2))%R.
-apply Rplus_le_compat ; apply bpow_le ; omega.
+apply Rplus_le_compat ; apply bpow_le ; lia.
 apply Rle_trans with (2*bpow (e - 2))%R;[right; ring|idtac].
 apply Rle_trans with (bpow 1*bpow (e - 2))%R.
 apply Rmult_le_compat_r.
@@ -614,7 +633,7 @@ apply Ropp_lt_contravar.
 apply bpow_gt_0.
 apply Rle_ge; apply Rle_0_minus.
 apply bpow_le.
-omega.
+lia.
 replace f with 0%R.
 apply generic_format_0.
 unfold f.
@@ -842,7 +861,7 @@ assert (ex - 1 < fexp ex < ex)%Z.
   split ; apply (lt_bpow beta) ; rewrite <- M by easy.
   lra.
   apply Hex.
-omega.
+lia.
 rewrite 2!ulp_neq_0 by lra.
 apply f_equal.
 unfold cexp ; apply f_equal.
@@ -907,7 +926,7 @@ split.
 apply Rplus_le_reg_l with (bpow (fexp (e-1))).
 ring_simplify.
 apply Rle_trans with (bpow (e - 2) + bpow (e - 2))%R.
-apply Rplus_le_compat; apply bpow_le; omega.
+apply Rplus_le_compat; apply bpow_le; lia.
 apply Rle_trans with (2*bpow (e - 2))%R;[right; ring|idtac].
 apply Rle_trans with (bpow 1*bpow (e - 2))%R.
 apply Rmult_le_compat_r.
@@ -930,7 +949,7 @@ apply bpow_gt_0.
 apply Rle_ge; apply Rle_0_minus.
 rewrite Hxe.
 apply bpow_le.
-omega.
+lia.
 (* *)
 contradict Zp.
 rewrite Hxe, He; ring.
@@ -953,12 +972,12 @@ unfold ulp; rewrite Req_bool_true; trivial.
 case negligible_exp_spec.
 intros K.
 specialize (K (e-1)%Z).
-contradict K; omega.
+contradict K; lia.
 intros n Hn.
 rewrite H3; apply f_equal.
 case (Zle_or_lt n (e-1)); intros H6.
-apply valid_exp; omega.
-apply sym_eq, valid_exp; omega.
+apply valid_exp; lia.
+apply sym_eq, valid_exp; lia.
 Qed.
 
 (** The following one is false for x = 0 in FTZ *)
@@ -1081,7 +1100,7 @@ exfalso ; lra.
 intros n Hn H.
 assert (fexp (mag beta eps) = fexp n).
 apply valid_exp; try assumption.
-assert(mag beta eps-1 < fexp n)%Z;[idtac|omega].
+assert(mag beta eps-1 < fexp n)%Z;[idtac|lia].
 apply lt_bpow with beta.
 apply Rle_lt_trans with (2:=proj2 H).
 destruct (mag beta eps) as (e,He).
@@ -1105,7 +1124,6 @@ rewrite <- P, round_0; trivial.
 apply valid_rnd_DN.
 Qed.
 
-
 Theorem round_UP_plus_eps_pos :
   forall x, (0 <= x)%R -> F x ->
   forall eps, (0 < eps <= ulp x)%R ->
@@ -1147,7 +1165,7 @@ lra.
 intros n Hn H.
 assert (fexp (mag beta eps) = fexp n).
 apply valid_exp; try assumption.
-assert(mag beta eps-1 < fexp n)%Z;[idtac|omega].
+assert(mag beta eps-1 < fexp n)%Z;[idtac|lia].
 apply lt_bpow with beta.
 apply Rle_lt_trans with (2:=H).
 destruct (mag beta eps) as (e,He).
@@ -1172,7 +1190,6 @@ apply round_generic...
 apply generic_format_ulp_0.
 Qed.
 
-
 Theorem round_UP_pred_plus_eps_pos :
   forall x, (0 < x)%R -> F x ->
   forall eps, (0 < eps <= ulp (pred x) )%R ->
@@ -1210,7 +1227,6 @@ apply Ropp_lt_contravar.
 now apply Heps.
 Qed.
 
-
 Theorem round_DN_plus_eps:
   forall x, F x ->
   forall eps, (0 <= eps < if (Rle_bool 0 x) then (ulp x)
@@ -1248,7 +1264,6 @@ now apply Ropp_0_gt_lt_contravar.
 now apply generic_format_opp.
 Qed.
 
-
 Theorem round_UP_plus_eps :
   forall x, F x ->
   forall eps, (0 < eps <= if (Rle_bool 0 x) then (ulp x)
@@ -1334,11 +1349,11 @@ now apply Rgt_not_eq.
 case (Zle_lt_or_eq _ _ H2); intros Hexy.
 assert (fexp ex = fexp (ey-1))%Z.
 apply valid_exp.
-omega.
+lia.
 rewrite <- H1.
-omega.
+lia.
 absurd (0 < Ztrunc (scaled_mantissa beta fexp x) < 1)%Z.
-omega.
+lia.
 split.
 apply gt_0_F2R with beta (cexp beta fexp x).
 now rewrite <- Fx.
@@ -1380,9 +1395,9 @@ apply sym_eq; apply mag_unique.
 rewrite H1, Rabs_right.
 split.
 apply bpow_le.
-omega.
+lia.
 apply bpow_lt.
-omega.
+lia.
 apply Rle_ge; apply bpow_ge_0.
 apply mag_unique.
 apply Hey.
@@ -1527,7 +1542,7 @@ rewrite mag_bpow.
 replace (fexp n + 1 - 1)%Z with (fexp n) by ring.
 rewrite Req_bool_true; trivial.
 apply Rminus_diag_eq, f_equal.
-apply sym_eq, valid_exp; omega.
+apply sym_eq, valid_exp; lia.
 Qed.
 
 Theorem succ_0 :
@@ -1904,7 +1919,7 @@ rewrite ulp_neq_0; trivial.
 apply f_equal.
 unfold cexp.
 apply valid_exp; trivial.
-assert (mag beta x -1 < fexp n)%Z;[idtac|omega].
+assert (mag beta x -1 < fexp n)%Z;[idtac|lia].
 apply lt_bpow with beta.
 destruct (mag beta x) as (e,He).
 simpl.
@@ -2252,9 +2267,9 @@ rewrite Hn1; easy.
 now apply ulp_ge_ulp_0.
 Qed.
 
-
-Lemma ulp_succ_pos : forall x, F x -> (0 < x)%R ->
-   ulp (succ x) = ulp x \/ succ x = bpow (mag beta x).
+Lemma ulp_succ_pos :
+  forall x, F x -> (0 < x)%R ->
+  ulp (succ x) = ulp x \/ succ x = bpow (mag beta x).
 Proof with auto with typeclass_instances.
 intros x Fx Hx.
 generalize (Rlt_le _ _ Hx); intros Hx'.
@@ -2281,6 +2296,39 @@ apply ulp_ge_0.
 now apply sym_eq, mag_unique_pos.
 Qed.
 
+Theorem ulp_pred_pos :
+  forall x, F x -> (0 < pred x)%R ->
+  ulp (pred x) = ulp x \/ x = bpow (mag beta x - 1).
+Proof.
+intros x Fx Hx.
+assert (Hx': (0 < x)%R).
+  apply Rlt_le_trans with (1 := Hx).
+  apply pred_le_id.
+assert (Zx : x <> 0%R).
+  now apply Rgt_not_eq.
+rewrite (ulp_neq_0 x) by easy.
+unfold cexp.
+destruct (mag beta x) as [e He].
+simpl.
+assert (bpow (e - 1) <= x < bpow e)%R.
+  rewrite <- (Rabs_pos_eq x) by now apply Rlt_le.
+  now apply He.
+destruct (proj1 H) as [H1|H1].
+2: now right.
+left.
+apply pred_ge_gt with (2 := Fx) in H1.
+rewrite ulp_neq_0 by now apply Rgt_not_eq.
+apply (f_equal (fun e => bpow (fexp e))).
+apply mag_unique_pos.
+apply (conj H1).
+apply Rle_lt_trans with (2 := proj2 H).
+apply pred_le_id.
+apply generic_format_bpow.
+apply Z.lt_le_pred.
+replace (_ + 1)%Z with e by ring.
+rewrite <- (mag_unique_pos _ _ _ H).
+now apply mag_generic_gt.
+Qed.
 
 Lemma ulp_round_pos :
   forall { Not_FTZ_ : Exp_not_FTZ fexp},
@@ -2333,7 +2381,6 @@ replace (fexp n) with (fexp e); try assumption.
 now apply fexp_negligible_exp_eq.
 Qed.
 
-
 Theorem ulp_round : forall { Not_FTZ_ : Exp_not_FTZ fexp},
    forall rnd { Zrnd : Valid_rnd rnd } x,
      ulp (round beta fexp rnd x) = ulp x
@@ -2373,6 +2420,18 @@ destruct (round_DN_or_UP beta fexp rnd x) as [Hr|Hr]; rewrite Hr.
 apply succ_ge_id.
 Qed.
 
+Lemma pred_round_le_id :
+  forall rnd { Zrnd : Valid_rnd rnd } x,
+  (pred (round beta fexp rnd x) <= x)%R.
+Proof.
+intros rnd Vrnd x.
+apply (Rle_trans _ (round beta fexp Raux.Zfloor x)).
+2: now apply round_DN_pt.
+destruct (round_DN_or_UP beta fexp rnd x) as [Hr|Hr]; rewrite Hr.
+2: now apply pred_UP_le_DN.
+apply pred_le_id.
+Qed.
+
 (** Properties of rounding to nearest and ulp *)
 
 Theorem round_N_le_midp: forall choice u v,
@@ -2432,6 +2491,73 @@ unfold pred.
 right; field.
 Qed.
 
+Lemma round_N_ge_ge_midp : forall choice u v,
+       F u ->
+       (u <= round beta fexp (Znearest choice) v)%R ->
+       ((u + pred u) / 2 <= v)%R.
+Proof with auto with typeclass_instances.
+intros choice u v Hu H2.
+assert (K: ((u=0)%R /\ negligible_exp = None) \/ (pred u < u)%R).
+case (Req_dec u 0); intros Zu.
+case_eq (negligible_exp).
+intros n Hn; right.
+rewrite Zu, pred_0.
+unfold ulp; rewrite Req_bool_true, Hn; try easy.
+rewrite <- Ropp_0.
+apply Ropp_lt_contravar, bpow_gt_0.
+intros _; left; split; easy.
+right.
+apply pred_lt_id...
+(* *)
+case K.
+intros (K1,K2).
+(* . *)
+rewrite K1, pred_0.
+unfold ulp; rewrite Req_bool_true, K2; try easy.
+replace ((0+-0)/2)%R with 0%R by field.
+case (Rle_or_lt 0 v); try easy.
+intros H3; contradict H2.
+rewrite K1; apply Rlt_not_le.
+assert (H4: (round beta fexp (Znearest choice) v <= 0)%R).
+apply round_le_generic...
+apply generic_format_0...
+now left.
+case H4; try easy.
+intros H5.
+absurd (v=0)%R; try auto with real.
+apply eq_0_round_0_negligible_exp with (Znearest choice)...
+(* . *)
+intros K1.
+case (Rle_or_lt ((u + pred u) / 2) v); try easy.
+intros H3.
+absurd (u <= round beta fexp (Znearest choice) v)%R; try easy.
+apply Rlt_not_le.
+apply Rle_lt_trans with (2:=K1).
+apply round_N_le_midp...
+apply generic_format_pred...
+rewrite succ_pred...
+apply Rlt_le_trans with (1:=H3).
+right; f_equal; ring.
+Qed.
+
+
+Lemma round_N_le_le_midp : forall choice u v,
+       F u ->
+       (round beta fexp (Znearest choice) v <= u)%R ->
+       (v <= (u + succ u) / 2)%R.
+Proof with auto with typeclass_instances.
+intros choice u v Hu H2.
+apply Ropp_le_cancel.
+apply Rle_trans with (((-u)+pred (-u))/2)%R.
+rewrite pred_opp; right; field.
+apply round_N_ge_ge_midp with
+   (choice := fun t:Z => negb (choice (- (t + 1))%Z))...
+apply generic_format_opp...
+rewrite <- (Ropp_involutive (round _ _ _ _)).
+rewrite <- round_N_opp, Ropp_involutive.
+apply Ropp_le_contravar; easy.
+Qed.
+
 
 Lemma round_N_eq_DN: forall choice x,
        let d:=round beta fexp Zfloor x in
@@ -2518,4 +2644,18 @@ rewrite round_generic; [now apply succ_le_plus_ulp|now simpl|].
 now apply generic_format_plus_ulp, generic_format_round.
 Qed.
 
+
+Lemma round_N_eq_ties: forall c1 c2 x,
+   (x - round beta fexp Zfloor x <> round beta fexp Zceil x - x)%R ->
+   (round beta fexp (Znearest c1) x = round beta fexp (Znearest c2) x)%R.
+Proof with auto with typeclass_instances.
+intros c1 c2 x.
+pose (d:=round beta fexp Zfloor x); pose (u:=round beta fexp Zceil x); fold d; fold u; intros H.
+case (Rle_or_lt ((d+u)/2) x); intros L.
+2:rewrite 2!round_N_eq_DN...
+destruct L as [L|L].
+rewrite 2!round_N_eq_UP...
+contradict H; rewrite <- L; field.
+Qed.
+
 End Fcore_ulp.
diff --git a/flocq/Core/Zaux.v b/flocq/Core/Zaux.v
index e21d93a4..b40b0c4f 100644
--- a/flocq/Core/Zaux.v
+++ b/flocq/Core/Zaux.v
@@ -17,8 +17,12 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 COPYING file for more details.
 *)
 
-Require Import ZArith Omega.
-Require Import Zquot.
+From Coq Require Import ZArith Lia Zquot.
+
+Require Import SpecFloatCompat.
+
+Notation cond_Zopp := cond_Zopp (only parsing).
+Notation iter_pos := iter_pos (only parsing).
 
 Section Zmissing.
 
@@ -262,7 +266,7 @@ apply Z.le_refl.
 split.
 easy.
 apply Zpower_gt_1.
-clear -He ; omega.
+clear -He ; lia.
 apply Zle_minus_le_0.
 now apply Zlt_le_weak.
 revert H1.
@@ -282,7 +286,7 @@ apply Znot_gt_le.
 intros H.
 apply Zlt_not_le with (1 := He).
 apply Zpower_le.
-clear -H ; omega.
+clear -H ; lia.
 Qed.
 
 Theorem Zpower_gt_id :
@@ -302,7 +306,7 @@ clear.
 apply Zlt_0_minus_lt.
 replace (r * (Z_of_nat n0 + 1) - (Z_of_nat n0 + 1))%Z with ((r - 1) * (Z_of_nat n0 + 1))%Z by ring.
 apply Zmult_lt_0_compat.
-cut (2 <= r)%Z. omega.
+cut (2 <= r)%Z. lia.
 apply Zle_bool_imp_le.
 apply r.
 apply (Zle_lt_succ 0).
@@ -420,7 +424,7 @@ apply Z.opp_inj.
 rewrite <- Zquot_opp_l, Z.opp_0.
 apply Z.quot_small.
 generalize (Zabs_non_eq a).
-omega.
+lia.
 Qed.
 
 Theorem ZOmod_small_abs :
@@ -437,7 +441,7 @@ apply Z.opp_inj.
 rewrite <- Zrem_opp_l.
 apply Z.rem_small.
 generalize (Zabs_non_eq a).
-omega.
+lia.
 Qed.
 
 Theorem ZOdiv_plus :
@@ -702,8 +706,6 @@ End Zcompare.
 
 Section cond_Zopp.
 
-Definition cond_Zopp (b : bool) m := if b then Z.opp m else m.
-
 Theorem cond_Zopp_negb :
   forall x y, cond_Zopp (negb x) y = Z.opp (cond_Zopp x y).
 Proof.
@@ -921,16 +923,9 @@ intros x.
 apply IHp.
 Qed.
 
-Fixpoint iter_pos (n : positive) (x : A) {struct n} : A :=
-  match n with
-  | xI n' => iter_pos n' (iter_pos n' (f x))
-  | xO n' => iter_pos n' (iter_pos n' x)
-  | xH => f x
-  end.
-
 Lemma iter_pos_nat :
   forall (p : positive) (x : A),
-  iter_pos p x = iter_nat (Pos.to_nat p) x.
+  iter_pos f p x = iter_nat (Pos.to_nat p) x.
 Proof.
 induction p ; intros x.
 rewrite Pos2Nat.inj_xI.
diff --git a/flocq/IEEE754/Binary.v b/flocq/IEEE754/Binary.v
index ac38c761..35d15cb3 100644
--- a/flocq/IEEE754/Binary.v
+++ b/flocq/IEEE754/Binary.v
@@ -627,6 +627,52 @@ Proof.
   now rewrite Pcompare_antisym.
 Qed.
 
+Theorem bounded_le_emax_minus_prec :
+  forall mx ex,
+  bounded mx ex = true ->
+  (F2R (Float radix2 (Zpos mx) ex)
+   <= bpow radix2 emax - bpow radix2 (emax - prec))%R.
+Proof.
+intros mx ex Hx.
+destruct (andb_prop _ _ Hx) as (H1,H2).
+generalize (Zeq_bool_eq _ _ H1). clear H1. intro H1.
+generalize (Zle_bool_imp_le _ _ H2). clear H2. intro H2.
+generalize (mag_F2R_Zdigits radix2 (Zpos mx) ex).
+destruct (mag radix2 (F2R (Float radix2 (Zpos mx) ex))) as (e',Ex).
+unfold mag_val.
+intros H.
+elim Ex; [|now apply Rgt_not_eq, F2R_gt_0]; intros _.
+rewrite <-F2R_Zabs; simpl; clear Ex; intros Ex.
+generalize (Rmult_lt_compat_r (bpow radix2 (-ex)) _ _ (bpow_gt_0 _ _) Ex).
+unfold F2R; simpl; rewrite Rmult_assoc, <-!bpow_plus.
+rewrite H; [|intro H'; discriminate H'].
+rewrite <-Z.add_assoc, Z.add_opp_diag_r, Z.add_0_r, Rmult_1_r.
+rewrite <-(IZR_Zpower _ _ (Zdigits_ge_0 _ _)); clear Ex; intro Ex.
+generalize (Zlt_le_succ _ _ (lt_IZR _ _ Ex)); clear Ex; intro Ex.
+generalize (IZR_le _ _ Ex).
+rewrite succ_IZR; clear Ex; intro Ex.
+generalize (Rplus_le_compat_r (-1) _ _ Ex); clear Ex; intro Ex.
+ring_simplify in Ex; revert Ex.
+rewrite (IZR_Zpower _ _ (Zdigits_ge_0 _ _)); intro Ex.
+generalize (Rmult_le_compat_r (bpow radix2 ex) _ _ (bpow_ge_0 _ _) Ex).
+intro H'; apply (Rle_trans _ _ _ H').
+rewrite Rmult_minus_distr_r, Rmult_1_l, <-bpow_plus.
+revert H1; unfold fexp, FLT_exp; intro H1.
+generalize (Z.le_max_l (Z.pos (digits2_pos mx) + ex - prec) emin).
+rewrite H1; intro H1'.
+generalize (proj1 (Z.le_sub_le_add_r _ _ _) H1').
+rewrite Zpos_digits2_pos; clear H1'; intro H1'.
+apply (Rle_trans _ _ _ (Rplus_le_compat_r _ _ _ (bpow_le _ _ _ H1'))).
+replace emax with (emax - prec - ex + (ex + prec))%Z at 1 by ring.
+replace (emax - prec)%Z with (emax - prec - ex + ex)%Z at 2 by ring.
+do 2 rewrite (bpow_plus _ (emax - prec - ex)).
+rewrite <-Rmult_minus_distr_l.
+rewrite <-(Rmult_1_l (_ + _)).
+apply Rmult_le_compat_r.
+{ apply Rle_0_minus, bpow_le; unfold Prec_gt_0 in prec_gt_0_; lia. }
+change 1%R with (bpow radix2 0); apply bpow_le; lia.
+Qed.
+
 Theorem bounded_lt_emax :
   forall mx ex,
   bounded mx ex = true ->
@@ -651,7 +697,7 @@ rewrite H. 2: discriminate.
 revert H1. clear -H2.
 rewrite Zpos_digits2_pos.
 unfold fexp, FLT_exp.
-intros ; zify ; omega.
+intros ; zify ; lia.
 Qed.
 
 Theorem bounded_ge_emin :
@@ -679,7 +725,18 @@ unfold fexp, FLT_exp.
 clear -prec_gt_0_.
 unfold Prec_gt_0 in prec_gt_0_.
 clearbody emin.
-intros ; zify ; omega.
+intros ; zify ; lia.
+Qed.
+
+Theorem abs_B2R_le_emax_minus_prec :
+  forall x,
+  (Rabs (B2R x) <= bpow radix2 emax - bpow radix2 (emax - prec))%R.
+Proof.
+intros [sx|sx|sx plx Hx|sx mx ex Hx] ; simpl ;
+  [rewrite Rabs_R0 ; apply Rle_0_minus, bpow_le ;
+   revert prec_gt_0_; unfold Prec_gt_0; lia..|].
+rewrite <- F2R_Zabs, abs_cond_Zopp.
+now apply bounded_le_emax_minus_prec.
 Qed.
 
 Theorem abs_B2R_lt_emax :
@@ -728,7 +785,7 @@ rewrite Cx.
 unfold cexp, fexp, FLT_exp.
 destruct (mag radix2 (F2R (Float radix2 (Zpos mx) ex))) as (e',Ex). simpl.
 apply Z.max_lub.
-cut (e' - 1 < emax)%Z. clear ; omega.
+cut (e' - 1 < emax)%Z. clear ; lia.
 apply lt_bpow with radix2.
 apply Rle_lt_trans with (2 := Bx).
 change (Zpos mx) with (Z.abs (Zpos mx)).
@@ -738,7 +795,7 @@ apply Rgt_not_eq.
 now apply F2R_gt_0.
 unfold emin.
 generalize (prec_gt_0 prec).
-clear -Hmax ; omega.
+clear -Hmax ; lia.
 Qed.
 
 (** Truncation *)
@@ -889,7 +946,7 @@ now inversion H.
 (* *)
 intros p Hp.
 assert (He: (e <= fexp (Zdigits radix2 m + e))%Z).
-clear -Hp ; zify ; omega.
+clear -Hp ; zify ; lia.
 destruct (inbetween_float_ex radix2 m e l) as (x, Hx).
 generalize (inbetween_shr x m e l (fexp (Zdigits radix2 m + e) - e) Hm Hx).
 assert (Hx0 : (0 <= x)%R).
@@ -1091,18 +1148,18 @@ rewrite Zpos_digits2_pos.
 replace (Zdigits radix2 (Zpos (match (Zpower 2 prec - 1)%Z with Zpos p => p | _ => xH end))) with prec.
 unfold fexp, FLT_exp, emin.
 generalize (prec_gt_0 prec).
-clear -Hmax ; zify ; omega.
+clear -Hmax ; zify ; lia.
 change 2%Z with (radix_val radix2).
 case_eq (Zpower radix2 prec - 1)%Z.
 simpl Zdigits.
 generalize (Zpower_gt_1 radix2 prec (prec_gt_0 prec)).
-clear ; omega.
+clear ; lia.
 intros p Hp.
 apply Zle_antisym.
-cut (prec - 1 < Zdigits radix2 (Zpos p))%Z. clear ; omega.
+cut (prec - 1 < Zdigits radix2 (Zpos p))%Z. clear ; lia.
 apply Zdigits_gt_Zpower.
 simpl Z.abs. rewrite <- Hp.
-cut (Zpower radix2 (prec - 1) < Zpower radix2 prec)%Z. clear ; omega.
+cut (Zpower radix2 (prec - 1) < Zpower radix2 prec)%Z. clear ; lia.
 apply lt_IZR.
 rewrite 2!IZR_Zpower. 2: now apply Zlt_le_weak.
 apply bpow_lt.
@@ -1113,7 +1170,7 @@ simpl Z.abs. rewrite <- Hp.
 apply Zlt_pred.
 intros p Hp.
 generalize (Zpower_gt_1 radix2 _ (prec_gt_0 prec)).
-clear -Hp ; zify ; omega.
+clear -Hp ; zify ; lia.
 apply Rnot_lt_le.
 intros Hx.
 generalize (refl_equal (bounded m2 e2)).
@@ -1271,18 +1328,18 @@ rewrite Zpos_digits2_pos.
 replace (Zdigits radix2 (Zpos (match (Zpower 2 prec - 1)%Z with Zpos p => p | _ => xH end))) with prec.
 unfold fexp, FLT_exp, emin.
 generalize (prec_gt_0 prec).
-clear -Hmax ; zify ; omega.
+clear -Hmax ; zify ; lia.
 change 2%Z with (radix_val radix2).
 case_eq (Zpower radix2 prec - 1)%Z.
 simpl Zdigits.
 generalize (Zpower_gt_1 radix2 prec (prec_gt_0 prec)).
-clear ; omega.
+clear ; lia.
 intros p Hp.
 apply Zle_antisym.
-cut (prec - 1 < Zdigits radix2 (Zpos p))%Z. clear ; omega.
+cut (prec - 1 < Zdigits radix2 (Zpos p))%Z. clear ; lia.
 apply Zdigits_gt_Zpower.
 simpl Z.abs. rewrite <- Hp.
-cut (Zpower radix2 (prec - 1) < Zpower radix2 prec)%Z. clear ; omega.
+cut (Zpower radix2 (prec - 1) < Zpower radix2 prec)%Z. clear ; lia.
 apply lt_IZR.
 rewrite 2!IZR_Zpower. 2: now apply Zlt_le_weak.
 apply bpow_lt.
@@ -1293,7 +1350,7 @@ simpl Z.abs. rewrite <- Hp.
 apply Zlt_pred.
 intros p Hp.
 generalize (Zpower_gt_1 radix2 _ (prec_gt_0 prec)).
-clear -Hp ; zify ; omega.
+clear -Hp ; zify ; lia.
 apply Rnot_lt_le.
 intros Hx.
 generalize (refl_equal (bounded m2 e2)).
@@ -1370,7 +1427,7 @@ clear -Hmax.
 unfold emin.
 intros dx dy dxy Hx Hy Hxy.
 zify ; intros ; subst.
-omega.
+lia.
 (* *)
 case sx ; case sy.
 apply Rlt_bool_false.
@@ -1479,7 +1536,7 @@ case_eq (ex' - ex)%Z ; simpl.
 intros H.
 now rewrite Zminus_eq with (1 := H).
 intros p.
-clear -He ; zify ; omega.
+clear -He ; zify ; lia.
 intros.
 apply refl_equal.
 Qed.
@@ -1580,7 +1637,7 @@ now rewrite is_finite_FF2B.
 rewrite Bsign_FF2B, Rz''.
 rewrite Rcompare_Gt...
 apply F2R_gt_0.
-simpl. zify; omega.
+simpl. zify; lia.
 intros Hz' (Vz, Rz).
 rewrite B2FF_FF2B, Rz.
 apply f_equal.
@@ -1599,7 +1656,7 @@ now rewrite is_finite_FF2B.
 rewrite Bsign_FF2B, Rz''.
 rewrite Rcompare_Lt...
 apply F2R_lt_0.
-simpl. zify; omega.
+simpl. zify; lia.
 intros Hz' (Vz, Rz).
 rewrite B2FF_FF2B, Rz.
 apply f_equal.
@@ -2150,7 +2207,7 @@ set (e' := Z.min _ _).
 assert (2 * e' <= ex)%Z as He.
 { assert (e' <= Z.div2 ex)%Z by apply Z.le_min_r.
   rewrite (Zdiv2_odd_eqn ex).
-  destruct Z.odd ; omega. }
+  destruct Z.odd ; lia. }
 generalize (Fsqrt_core_correct radix2 (Zpos mx) ex e' eq_refl He).
 unfold Fsqrt_core.
 set (mx' := match (ex - 2 * e')%Z with Z0 => _ | _ => _ end).
@@ -2187,7 +2244,7 @@ apply Rlt_le_trans with (1 := Heps).
 fold (bpow radix2 0).
 apply bpow_le.
 generalize (prec_gt_0 prec).
-clear ; omega.
+clear ; lia.
 apply Rsqr_incrst_0.
 3: apply bpow_ge_0.
 rewrite Rsqr_mult.
@@ -2211,7 +2268,7 @@ now apply IZR_le.
 change 4%R with (bpow radix2 2).
 apply bpow_le.
 generalize (prec_gt_0 prec).
-clear -Hmax ; omega.
+clear -Hmax ; lia.
 apply Rmult_le_pos.
 apply sqrt_ge_0.
 rewrite <- (Rplus_opp_r 1).
@@ -2230,7 +2287,7 @@ unfold Rsqr.
 rewrite <- bpow_plus.
 apply bpow_le.
 unfold emin.
-clear -Hmax ; omega.
+clear -Hmax ; lia.
 apply generic_format_ge_bpow with fexp.
 intros.
 apply Z.le_max_r.
diff --git a/flocq/IEEE754/Bits.v b/flocq/IEEE754/Bits.v
index 3a84edfe..68bc541a 100644
--- a/flocq/IEEE754/Bits.v
+++ b/flocq/IEEE754/Bits.v
@@ -18,6 +18,8 @@ COPYING file for more details.
 *)
 
 (** * IEEE-754 encoding of binary floating-point data *)
+
+From Coq Require Import Lia.
 Require Import Core Digits Binary.
 
 Section Binary_Bits.
@@ -43,10 +45,10 @@ Proof.
 intros s m e Hm He.
 assert (0 <= mw)%Z as Hmw.
   destruct mw as [|mw'|mw'] ; try easy.
-  clear -Hm ; simpl in Hm ; omega.
+  clear -Hm ; simpl in Hm ; lia.
 assert (0 <= ew)%Z as Hew.
   destruct ew as [|ew'|ew'] ; try easy.
-  clear -He ; simpl in He ; omega.
+  clear -He ; simpl in He ; lia.
 unfold join_bits.
 rewrite Z.shiftl_mul_pow2 by easy.
 split.
@@ -54,9 +56,9 @@ split.
   rewrite <- (Zmult_0_l (2^mw)).
   apply Zmult_le_compat_r.
   case s.
-  clear -He ; omega.
+  clear -He ; lia.
   now rewrite Zmult_0_l.
-  clear -Hm ; omega.
+  clear -Hm ; lia.
 - apply Z.lt_le_trans with (((if s then 2 ^ ew else 0) + e + 1) * 2 ^ mw)%Z.
   rewrite (Zmult_plus_distr_l _ 1).
   apply Zplus_lt_compat_l.
@@ -65,9 +67,9 @@ split.
   apply Zmult_le_compat_r.
   rewrite Zpower_plus by easy.
   change (2^1)%Z with 2%Z.
-  case s ; clear -He ; omega.
-  clear -Hm ; omega.
-  clear -Hew ; omega.
+  case s ; clear -He ; lia.
+  clear -Hm ; lia.
+  clear -Hew ; lia.
   easy.
 Qed.
 
@@ -85,10 +87,10 @@ Proof.
 intros s m e Hm He.
 assert (0 <= mw)%Z as Hmw.
   destruct mw as [|mw'|mw'] ; try easy.
-  clear -Hm ; simpl in Hm ; omega.
+  clear -Hm ; simpl in Hm ; lia.
 assert (0 <= ew)%Z as Hew.
   destruct ew as [|ew'|ew'] ; try easy.
-  clear -He ; simpl in He ; omega.
+  clear -He ; simpl in He ; lia.
 unfold split_bits, join_bits.
 rewrite Z.shiftl_mul_pow2 by easy.
 apply f_equal2 ; [apply f_equal2|].
@@ -99,7 +101,7 @@ apply f_equal2 ; [apply f_equal2|].
     apply Zplus_le_0_compat.
     apply Zmult_le_0_compat.
     apply He.
-    clear -Hm ; omega.
+    clear -Hm ; lia.
     apply Hm.
   + apply Zle_bool_false.
     apply Zplus_lt_reg_l with (2^mw * (-e))%Z.
@@ -108,12 +110,12 @@ apply f_equal2 ; [apply f_equal2|].
     apply Z.lt_le_trans with (2^mw * 1)%Z.
     now apply Zmult_lt_compat_r.
     apply Zmult_le_compat_l.
-    clear -He ; omega.
-    clear -Hm ; omega.
+    clear -He ; lia.
+    clear -Hm ; lia.
 - rewrite Zplus_comm.
   rewrite Z_mod_plus_full.
   now apply Zmod_small.
-- rewrite Z_div_plus_full_l by (clear -Hm ; omega).
+- rewrite Z_div_plus_full_l by (clear -Hm ; lia).
   rewrite Zdiv_small with (1 := Hm).
   rewrite Zplus_0_r.
   case s.
@@ -175,7 +177,7 @@ rewrite Zdiv_Zdiv.
 apply sym_eq.
 case Zle_bool_spec ; intros Hs.
 apply Zle_antisym.
-cut (x / (2^mw * 2^ew) < 2)%Z. clear ; omega.
+cut (x / (2^mw * 2^ew) < 2)%Z. clear ; lia.
 apply Zdiv_lt_upper_bound.
 now apply Zmult_lt_0_compat.
 rewrite <- Zpower_exp ; try ( apply Z.le_ge ; apply Zlt_le_weak ; assumption ).
@@ -244,8 +246,8 @@ Theorem split_bits_of_binary_float_correct :
   split_bits (bits_of_binary_float x) = split_bits_of_binary_float x.
 Proof.
 intros [sx|sx|sx plx Hplx|sx mx ex Hx] ;
-  try ( simpl ; apply split_join_bits ; split ; try apply Z.le_refl ; try apply Zlt_pred ; trivial ; omega ).
-simpl. apply split_join_bits; split; try (zify; omega).
+  try ( simpl ; apply split_join_bits ; split ; try apply Z.le_refl ; try apply Zlt_pred ; trivial ; lia ).
+simpl. apply split_join_bits; split; try (zify; lia).
 destruct (digits2_Pnat_correct plx).
 unfold nan_pl in Hplx.
 rewrite Zpos_digits2_pos, <- Z_of_nat_S_digits2_Pnat in Hplx.
@@ -253,7 +255,7 @@ rewrite Zpower_nat_Z in H0.
 eapply Z.lt_le_trans. apply H0.
 change 2%Z with (radix_val radix2). apply Zpower_le.
 rewrite Z.ltb_lt in Hplx.
-unfold prec in *. zify; omega.
+unfold prec in *. zify; lia.
 (* *)
 unfold bits_of_binary_float, split_bits_of_binary_float.
 assert (Hf: (emin <= ex /\ Zdigits radix2 (Zpos mx) <= prec)%Z).
@@ -263,14 +265,14 @@ rewrite Zpos_digits2_pos in Hx'.
 generalize (Zeq_bool_eq _ _ Hx').
 unfold FLT_exp.
 unfold emin.
-clear ; zify ; omega.
+clear ; zify ; lia.
 case Zle_bool_spec ; intros H ;
   [ apply -> Z.le_0_sub in H | apply -> Z.lt_sub_0 in H ] ;
   apply split_join_bits ; try now split.
 (* *)
 split.
-clear -He_gt_0 H ; omega.
-cut (Zpos mx < 2 * 2^mw)%Z. clear ; omega.
+clear -He_gt_0 H ; lia.
+cut (Zpos mx < 2 * 2^mw)%Z. clear ; lia.
 replace (2 * 2^mw)%Z with (2^prec)%Z.
 apply (Zpower_gt_Zdigits radix2 _ (Zpos mx)).
 apply Hf.
@@ -282,12 +284,12 @@ now apply Zlt_le_weak.
 (* *)
 split.
 generalize (proj1 Hf).
-clear ; omega.
+clear ; lia.
 destruct (andb_prop _ _ Hx) as (_, Hx').
 unfold emin.
 replace (2^ew)%Z with (2 * emax)%Z.
 generalize (Zle_bool_imp_le _ _ Hx').
-clear ; omega.
+clear ; lia.
 apply sym_eq.
 rewrite (Zsucc_pred ew).
 unfold Z.succ.
@@ -305,7 +307,7 @@ intros [sx|sx|sx pl pl_range|sx mx ex H].
 - apply join_bits_range ; now split.
 - apply join_bits_range.
   now split.
-  clear -He_gt_0 ; omega.
+  clear -He_gt_0 ; lia.
 - apply Z.ltb_lt in pl_range.
   apply join_bits_range.
   split.
@@ -313,7 +315,7 @@ intros [sx|sx|sx pl pl_range|sx mx ex H].
   apply (Zpower_gt_Zdigits radix2 _ (Zpos pl)).
   apply Z.lt_succ_r.
   now rewrite <- Zdigits2_Zdigits.
-  clear -He_gt_0 ; omega.
+  clear -He_gt_0 ; lia.
 - unfold bounded in H.
   apply Bool.andb_true_iff in H ; destruct H as [A B].
   apply Z.leb_le in B.
@@ -321,22 +323,22 @@ intros [sx|sx|sx pl pl_range|sx mx ex H].
   case Zle_bool_spec ; intros H.
   + apply join_bits_range.
     * split.
-      clear -H ; omega.
+      clear -H ; lia.
       rewrite Zpos_digits2_pos in A.
       cut (Zpos mx < 2 ^ prec)%Z.
       unfold prec.
-      rewrite Zpower_plus by (clear -Hmw ; omega).
+      rewrite Zpower_plus by (clear -Hmw ; lia).
       change (2^1)%Z with 2%Z.
-      clear ; omega.
+      clear ; lia.
       apply (Zpower_gt_Zdigits radix2 _ (Zpos mx)).
-      clear -A ; zify ; omega.
+      clear -A ; zify ; lia.
     * split.
-      unfold emin ; clear -A ; zify ; omega.
+      unfold emin ; clear -A ; zify ; lia.
       replace ew with ((ew - 1) + 1)%Z by ring.
-      rewrite Zpower_plus by (clear - Hew ; omega).
+      rewrite Zpower_plus by (clear - Hew ; lia).
       unfold emin, emax in *.
       change (2^1)%Z with 2%Z.
-      clear -B ; omega.
+      clear -B ; lia.
   + apply -> Z.lt_sub_0 in H.
     apply join_bits_range ; now split.
 Qed.
@@ -370,7 +372,7 @@ unfold binary_float_of_bits_aux, split_bits.
 assert (Hnan: nan_pl prec 1 = true).
   apply Z.ltb_lt.
   simpl. unfold prec.
-  clear -Hmw ; omega.
+  clear -Hmw ; lia.
 case Zeq_bool_spec ; intros He1.
 case_eq (x mod 2^mw)%Z ; try easy.
 (* subnormal *)
@@ -389,7 +391,7 @@ unfold Fexp, FLT_exp.
 apply sym_eq.
 apply Zmax_right.
 clear -H Hprec.
-unfold prec ; omega.
+unfold prec ; lia.
 apply Rnot_le_lt.
 intros H0.
 refine (_ (mag_le radix2 _ _ _ H0)).
@@ -397,20 +399,20 @@ rewrite mag_bpow.
 rewrite mag_F2R_Zdigits. 2: discriminate.
 unfold emin, prec.
 apply Zlt_not_le.
-cut (0 < emax)%Z. clear -H Hew ; omega.
+cut (0 < emax)%Z. clear -H Hew ; lia.
 apply (Zpower_gt_0 radix2).
-clear -Hew ; omega.
+clear -Hew ; lia.
 apply bpow_gt_0.
 case Zeq_bool_spec ; intros He2.
 case_eq (x mod 2 ^ mw)%Z; try easy.
 (* nan *)
 intros plx Eqplx. apply Z.ltb_lt.
 rewrite Zpos_digits2_pos.
-assert (forall a b, a <= b -> a < b+1)%Z by (intros; omega). apply H. clear H.
+assert (forall a b, a <= b -> a < b+1)%Z by (intros; lia). apply H. clear H.
 apply Zdigits_le_Zpower. simpl.
 rewrite <- Eqplx. edestruct Z_mod_lt; eauto.
 change 2%Z with (radix_val radix2).
-apply Z.lt_gt, Zpower_gt_0. omega.
+apply Z.lt_gt, Zpower_gt_0. lia.
 case_eq (x mod 2^mw + 2^mw)%Z ; try easy.
 (* normal *)
 intros px Hm.
@@ -452,7 +454,7 @@ revert He1.
 fold ex.
 cut (0 <= ex)%Z.
 unfold emin.
-clear ; intros H1 H2 ; omega.
+clear ; intros H1 H2 ; lia.
 eapply Z_mod_lt.
 apply Z.lt_gt.
 apply (Zpower_gt_0 radix2).
@@ -471,12 +473,12 @@ revert He2.
 set (ex := ((x / 2^mw) mod 2^ew)%Z).
 cut (ex < 2^ew)%Z.
 replace (2^ew)%Z with (2 * emax)%Z.
-clear ; intros H1 H2 ; omega.
+clear ; intros H1 H2 ; lia.
 replace ew with (1 + (ew - 1))%Z by ring.
 rewrite Zpower_exp.
 apply refl_equal.
 discriminate.
-clear -Hew ; omega.
+clear -Hew ; lia.
 eapply Z_mod_lt.
 apply Z.lt_gt.
 apply (Zpower_gt_0 radix2).
@@ -503,13 +505,13 @@ apply refl_equal.
 simpl.
 rewrite Zeq_bool_false.
 now rewrite Zeq_bool_true.
-cut (1 < 2^ew)%Z. clear ; omega.
+cut (1 < 2^ew)%Z. clear ; lia.
 now apply (Zpower_gt_1 radix2).
 (* *)
 simpl.
 rewrite Zeq_bool_false.
 rewrite Zeq_bool_true; auto.
-cut (1 < 2^ew)%Z. clear ; omega.
+cut (1 < 2^ew)%Z. clear ; lia.
 now apply (Zpower_gt_1 radix2).
 (* *)
 unfold split_bits_of_binary_float.
@@ -522,19 +524,19 @@ destruct (andb_prop _ _ Bx) as (_, H1).
 generalize (Zle_bool_imp_le _ _ H1).
 unfold emin.
 replace (2^ew)%Z with (2 * emax)%Z.
-clear ; omega.
+clear ; lia.
 replace ew with (1 + (ew - 1))%Z by ring.
 rewrite Zpower_exp.
 apply refl_equal.
 discriminate.
-clear -Hew ; omega.
+clear -Hew ; lia.
 destruct (andb_prop _ _ Bx) as (H1, _).
 generalize (Zeq_bool_eq _ _ H1).
 rewrite Zpos_digits2_pos.
 unfold FLT_exp, emin.
 generalize (Zdigits radix2 (Zpos mx)).
 clear.
-intros ; zify ; omega.
+intros ; zify ; lia.
 (* . *)
 rewrite Zeq_bool_true. 2: apply refl_equal.
 simpl.
@@ -547,7 +549,7 @@ apply -> Z.lt_sub_0 in Hm.
 generalize (Zdigits_le_Zpower radix2 _ (Zpos mx) Hm).
 generalize (Zdigits radix2 (Zpos mx)).
 clear.
-intros ; zify ; omega.
+intros ; zify ; lia.
 Qed.
 
 Theorem bits_of_binary_float_of_bits :
@@ -588,12 +590,12 @@ case Zeq_bool_spec ; intros He2.
 case_eq mx; intros Hm.
 now rewrite He2.
 now rewrite He2.
-intros. zify; omega.
+intros. zify; lia.
 (* normal *)
 case_eq (mx + 2 ^ mw)%Z.
 intros Hm.
 apply False_ind.
-clear -Bm Hm ; omega.
+clear -Bm Hm ; lia.
 intros p Hm Jx Cx.
 rewrite <- Hm.
 rewrite Zle_bool_true.
@@ -601,7 +603,7 @@ now ring_simplify (mx + 2^mw - 2^mw)%Z (ex + emin - 1 - emin + 1)%Z.
 now ring_simplify.
 intros p Hm.
 apply False_ind.
-clear -Bm Hm ; zify ; omega.
+clear -Bm Hm ; zify ; lia.
 Qed.
 
 End Binary_Bits.
@@ -623,6 +625,12 @@ Proof.
 apply refl_equal.
 Qed.
 
+Let Hemax : (3 <= 128)%Z.
+Proof.
+intros H.
+discriminate H.
+Qed.
+
 Definition default_nan_pl32 : { nan : binary32 | is_nan 24 128 nan = true } :=
   exist _ (@B754_nan 24 128 false (iter_nat xO 22 xH) (refl_equal true)) (refl_equal true).
 
@@ -639,16 +647,28 @@ Definition binop_nan_pl32 (f1 f2 : binary32) : { nan : binary32 | is_nan 24 128
   | _, _ => default_nan_pl32
   end.
 
+Definition ternop_nan_pl32 (f1 f2 f3 : binary32) : { nan : binary32 | is_nan 24 128 nan = true } :=
+  match f1, f2, f3 with
+  | B754_nan s1 pl1 Hpl1, _, _ => exist _ (B754_nan s1 pl1 Hpl1) (refl_equal true)
+  | _, B754_nan s2 pl2 Hpl2, _ => exist _ (B754_nan s2 pl2 Hpl2) (refl_equal true)
+  | _, _, B754_nan s3 pl3 Hpl3 => exist _ (B754_nan s3 pl3 Hpl3) (refl_equal true)
+  | _, _, _ => default_nan_pl32
+  end.
+
 Definition b32_erase : binary32 -> binary32 := erase 24 128.
 Definition b32_opp : binary32 -> binary32 := Bopp 24 128 unop_nan_pl32.
 Definition b32_abs : binary32 -> binary32 := Babs 24 128 unop_nan_pl32.
-Definition b32_sqrt :  mode -> binary32 -> binary32 := Bsqrt  _ _ Hprec Hprec_emax unop_nan_pl32.
+Definition b32_pred : binary32 -> binary32 := Bpred _ _ Hprec Hprec_emax Hemax unop_nan_pl32.
+Definition b32_succ : binary32 -> binary32 := Bsucc _ _ Hprec Hprec_emax Hemax unop_nan_pl32.
+Definition b32_sqrt : mode -> binary32 -> binary32 := Bsqrt  _ _ Hprec Hprec_emax unop_nan_pl32.
 
 Definition b32_plus :  mode -> binary32 -> binary32 -> binary32 := Bplus  _ _ Hprec Hprec_emax binop_nan_pl32.
 Definition b32_minus : mode -> binary32 -> binary32 -> binary32 := Bminus _ _ Hprec Hprec_emax binop_nan_pl32.
 Definition b32_mult :  mode -> binary32 -> binary32 -> binary32 := Bmult  _ _ Hprec Hprec_emax binop_nan_pl32.
 Definition b32_div :   mode -> binary32 -> binary32 -> binary32 := Bdiv   _ _ Hprec Hprec_emax binop_nan_pl32.
 
+Definition b32_fma :   mode -> binary32 -> binary32 -> binary32 -> binary32 := Bfma _ _ Hprec Hprec_emax ternop_nan_pl32.
+
 Definition b32_compare : binary32 -> binary32 -> option comparison := Bcompare 24 128.
 Definition b32_of_bits : Z -> binary32 := binary_float_of_bits 23 8 (refl_equal _) (refl_equal _) (refl_equal _).
 Definition bits_of_b32 : binary32 -> Z := bits_of_binary_float 23 8.
@@ -672,6 +692,12 @@ Proof.
 apply refl_equal.
 Qed.
 
+Let Hemax : (3 <= 1024)%Z.
+Proof.
+intros H.
+discriminate H.
+Qed.
+
 Definition default_nan_pl64 : { nan : binary64 | is_nan 53 1024 nan = true } :=
   exist _ (@B754_nan 53 1024 false (iter_nat xO 51 xH) (refl_equal true)) (refl_equal true).
 
@@ -688,9 +714,19 @@ Definition binop_nan_pl64 (f1 f2 : binary64) : { nan : binary64 | is_nan 53 1024
   | _, _ => default_nan_pl64
   end.
 
+Definition ternop_nan_pl64 (f1 f2 f3 : binary64) : { nan : binary64 | is_nan 53 1024 nan = true } :=
+  match f1, f2, f3 with
+  | B754_nan s1 pl1 Hpl1, _, _ => exist _ (B754_nan s1 pl1 Hpl1) (refl_equal true)
+  | _, B754_nan s2 pl2 Hpl2, _ => exist _ (B754_nan s2 pl2 Hpl2) (refl_equal true)
+  | _, _, B754_nan s3 pl3 Hpl3 => exist _ (B754_nan s3 pl3 Hpl3) (refl_equal true)
+  | _, _, _ => default_nan_pl64
+  end.
+
 Definition b64_erase : binary64 -> binary64 := erase 53 1024.
 Definition b64_opp : binary64 -> binary64 := Bopp 53 1024 unop_nan_pl64.
 Definition b64_abs : binary64 -> binary64 := Babs 53 1024 unop_nan_pl64.
+Definition b64_pred : binary64 -> binary64 := Bpred _ _ Hprec Hprec_emax Hemax unop_nan_pl64.
+Definition b64_succ : binary64 -> binary64 := Bsucc _ _ Hprec Hprec_emax Hemax unop_nan_pl64.
 Definition b64_sqrt : mode -> binary64 -> binary64 := Bsqrt _ _ Hprec Hprec_emax unop_nan_pl64.
 
 Definition b64_plus  : mode -> binary64 -> binary64 -> binary64 := Bplus  _ _ Hprec Hprec_emax binop_nan_pl64.
@@ -698,6 +734,8 @@ Definition b64_minus : mode -> binary64 -> binary64 -> binary64 := Bminus _ _ Hp
 Definition b64_mult  : mode -> binary64 -> binary64 -> binary64 := Bmult  _ _ Hprec Hprec_emax binop_nan_pl64.
 Definition b64_div   : mode -> binary64 -> binary64 -> binary64 := Bdiv   _ _ Hprec Hprec_emax binop_nan_pl64.
 
+Definition b64_fma :   mode -> binary64 -> binary64 -> binary64 -> binary64 := Bfma _ _ Hprec Hprec_emax ternop_nan_pl64.
+
 Definition b64_compare : binary64 -> binary64 -> option comparison := Bcompare 53 1024.
 Definition b64_of_bits : Z -> binary64 := binary_float_of_bits 52 11 (refl_equal _) (refl_equal _) (refl_equal _).
 Definition bits_of_b64 : binary64 -> Z := bits_of_binary_float 52 11.
diff --git a/flocq/IEEE754/SpecFloatCompat.v b/flocq/IEEE754/SpecFloatCompat.v
new file mode 100644
index 00000000..e2ace4d5
--- /dev/null
+++ b/flocq/IEEE754/SpecFloatCompat.v
@@ -0,0 +1,435 @@
+(**
+This file is part of the Flocq formalization of floating-point
+arithmetic in Coq: http://flocq.gforge.inria.fr/
+
+Copyright (C) 2018-2019 Guillaume Bertholon
+#<br />#
+Copyright (C) 2018-2019 Érik Martin-Dorel
+#<br />#
+Copyright (C) 2018-2019 Pierre Roux
+
+This library is free software; you can redistribute it and/or
+modify it under the terms of the GNU Lesser General Public
+License as published by the Free Software Foundation; either
+version 3 of the License, or (at your option) any later version.
+
+This library is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+COPYING file for more details.
+*)
+
+Require Import ZArith.
+
+(** ** Inductive specification of floating-point numbers
+
+Similar to [IEEE754.Binary.full_float], but with no NaN payload. *)
+Variant spec_float :=
+  | S754_zero (s : bool)
+  | S754_infinity (s : bool)
+  | S754_nan
+  | S754_finite (s : bool) (m : positive) (e : Z).
+
+(** ** Parameterized definitions
+
+[prec] is the number of bits of the mantissa including the implicit one;
+[emax] is the exponent of the infinities.
+
+For instance, Binary64 is defined by [prec = 53] and [emax = 1024]. *)
+Section FloatOps.
+  Variable prec emax : Z.
+
+  Definition emin := (3-emax-prec)%Z.
+  Definition fexp e := Z.max (e - prec) emin.
+
+  Section Zdigits2.
+    Fixpoint digits2_pos (n : positive) : positive :=
+      match n with
+      | xH => xH
+      | xO p => Pos.succ (digits2_pos p)
+      | xI p => Pos.succ (digits2_pos p)
+      end.
+
+    Definition Zdigits2 n :=
+      match n with
+      | Z0 => n
+      | Zpos p => Zpos (digits2_pos p)
+      | Zneg p => Zpos (digits2_pos p)
+      end.
+  End Zdigits2.
+
+  Section ValidBinary.
+    Definition canonical_mantissa m e :=
+      Zeq_bool (fexp (Zpos (digits2_pos m) + e)) e.
+
+    Definition bounded m e :=
+      andb (canonical_mantissa m e) (Zle_bool e (emax - prec)).
+
+    Definition valid_binary x :=
+      match x with
+      | S754_finite _ m e => bounded m e
+      | _ => true
+      end.
+  End ValidBinary.
+
+  Section Iter.
+    Context {A : Type}.
+    Variable (f : A -> A).
+
+    Fixpoint iter_pos (n : positive) (x : A) {struct n} : A :=
+      match n with
+      | xI n' => iter_pos n' (iter_pos n' (f x))
+      | xO n' => iter_pos n' (iter_pos n' x)
+      | xH => f x
+      end.
+  End Iter.
+
+  Section Rounding.
+    Inductive location := loc_Exact | loc_Inexact : comparison -> location.
+
+    Record shr_record := { shr_m : Z ; shr_r : bool ; shr_s : bool }.
+
+    Definition shr_1 mrs :=
+      let '(Build_shr_record m r s) := mrs in
+      let s := orb r s in
+      match m with
+      | Z0 => Build_shr_record Z0 false s
+      | Zpos xH => Build_shr_record Z0 true s
+      | Zpos (xO p) => Build_shr_record (Zpos p) false s
+      | Zpos (xI p) => Build_shr_record (Zpos p) true s
+      | Zneg xH => Build_shr_record Z0 true s
+      | Zneg (xO p) => Build_shr_record (Zneg p) false s
+      | Zneg (xI p) => Build_shr_record (Zneg p) true s
+      end.
+
+    Definition loc_of_shr_record mrs :=
+      match mrs with
+      | Build_shr_record _ false false => loc_Exact
+      | Build_shr_record _ false true => loc_Inexact Lt
+      | Build_shr_record _ true false => loc_Inexact Eq
+      | Build_shr_record _ true true => loc_Inexact Gt
+      end.
+
+    Definition shr_record_of_loc m l :=
+      match l with
+      | loc_Exact => Build_shr_record m false false
+      | loc_Inexact Lt => Build_shr_record m false true
+      | loc_Inexact Eq => Build_shr_record m true false
+      | loc_Inexact Gt => Build_shr_record m true true
+      end.
+
+    Definition shr mrs e n :=
+      match n with
+      | Zpos p => (iter_pos shr_1 p mrs, (e + n)%Z)
+      | _ => (mrs, e)
+      end.
+
+    Definition shr_fexp m e l :=
+      shr (shr_record_of_loc m l) e (fexp (Zdigits2 m + e) - e).
+
+    Definition round_nearest_even mx lx :=
+      match lx with
+      | loc_Exact => mx
+      | loc_Inexact Lt => mx
+      | loc_Inexact Eq => if Z.even mx then mx else (mx + 1)%Z
+      | loc_Inexact Gt => (mx + 1)%Z
+      end.
+
+    Definition binary_round_aux sx mx ex lx :=
+      let '(mrs', e') := shr_fexp mx ex lx in
+      let '(mrs'', e'') := shr_fexp (round_nearest_even (shr_m mrs') (loc_of_shr_record mrs')) e' loc_Exact in
+      match shr_m mrs'' with
+      | Z0 => S754_zero sx
+      | Zpos m => if Zle_bool e'' (emax - prec) then S754_finite sx m e'' else S754_infinity sx
+      | _ => S754_nan
+      end.
+
+    Definition shl_align mx ex ex' :=
+      match (ex' - ex)%Z with
+      | Zneg d => (shift_pos d mx, ex')
+      | _ => (mx, ex)
+      end.
+
+    Definition binary_round sx mx ex :=
+      let '(mz, ez) := shl_align mx ex (fexp (Zpos (digits2_pos mx) + ex))in
+      binary_round_aux sx (Zpos mz) ez loc_Exact.
+
+    Definition binary_normalize m e szero :=
+      match m with
+      | Z0 => S754_zero szero
+      | Zpos m => binary_round false m e
+      | Zneg m => binary_round true m e
+      end.
+  End Rounding.
+
+  (** ** Define operations *)
+
+  Definition SFopp x :=
+    match x with
+    | S754_nan => S754_nan
+    | S754_infinity sx => S754_infinity (negb sx)
+    | S754_finite sx mx ex => S754_finite (negb sx) mx ex
+    | S754_zero sx => S754_zero (negb sx)
+    end.
+
+  Definition SFabs x :=
+    match x with
+    | S754_nan => S754_nan
+    | S754_infinity sx => S754_infinity false
+    | S754_finite sx mx ex => S754_finite false mx ex
+    | S754_zero sx => S754_zero false
+    end.
+
+  Definition SFcompare f1 f2 :=
+    match f1, f2 with
+    | S754_nan , _ | _, S754_nan => None
+    | S754_infinity s1, S754_infinity s2 =>
+      Some match s1, s2 with
+      | true, true => Eq
+      | false, false => Eq
+      | true, false => Lt
+      | false, true => Gt
+      end
+    | S754_infinity s, _ => Some (if s then Lt else Gt)
+    | _, S754_infinity s => Some (if s then Gt else Lt)
+    | S754_finite s _ _, S754_zero _ => Some (if s then Lt else Gt)
+    | S754_zero _, S754_finite s _ _ => Some (if s then Gt else Lt)
+    | S754_zero _, S754_zero _ => Some Eq
+    | S754_finite s1 m1 e1, S754_finite s2 m2 e2 =>
+      Some match s1, s2 with
+      | true, false => Lt
+      | false, true => Gt
+      | false, false =>
+        match Z.compare e1 e2 with
+        | Lt => Lt
+        | Gt => Gt
+        | Eq => Pcompare m1 m2 Eq
+        end
+      | true, true =>
+        match Z.compare e1 e2 with
+        | Lt => Gt
+        | Gt => Lt
+        | Eq => CompOpp (Pcompare m1 m2 Eq)
+        end
+      end
+    end.
+
+  Definition SFeqb f1 f2 :=
+    match SFcompare f1 f2 with
+    | Some Eq => true
+    | _ => false
+    end.
+
+  Definition SFltb f1 f2 :=
+    match SFcompare f1 f2 with
+    | Some Lt => true
+    | _ => false
+    end.
+
+  Definition SFleb f1 f2 :=
+    match SFcompare f1 f2 with
+    | Some (Lt | Eq) => true
+    | _ => false
+    end.
+
+  Variant float_class : Set :=
+    | PNormal | NNormal | PSubn | NSubn | PZero | NZero | PInf | NInf | NaN.
+
+  Definition SFclassify f :=
+    match f with
+    | S754_nan => NaN
+    | S754_infinity false => PInf
+    | S754_infinity true => NInf
+    | S754_zero false => NZero
+    | S754_zero true => PZero
+    | S754_finite false m _ =>
+      if (digits2_pos m =? Z.to_pos prec)%positive then PNormal
+      else PSubn
+    | S754_finite true m _ =>
+      if (digits2_pos m =? Z.to_pos prec)%positive then NNormal
+      else NSubn
+    end.
+
+  Definition SFmul x y :=
+    match x, y with
+    | S754_nan, _ | _, S754_nan => S754_nan
+    | S754_infinity sx, S754_infinity sy => S754_infinity (xorb sx sy)
+    | S754_infinity sx, S754_finite sy _ _ => S754_infinity (xorb sx sy)
+    | S754_finite sx _ _, S754_infinity sy => S754_infinity (xorb sx sy)
+    | S754_infinity _, S754_zero _ => S754_nan
+    | S754_zero _, S754_infinity _ => S754_nan
+    | S754_finite sx _ _, S754_zero sy => S754_zero (xorb sx sy)
+    | S754_zero sx, S754_finite sy _ _ => S754_zero (xorb sx sy)
+    | S754_zero sx, S754_zero sy => S754_zero (xorb sx sy)
+    | S754_finite sx mx ex, S754_finite sy my ey =>
+      binary_round_aux (xorb sx sy) (Zpos (mx * my)) (ex + ey) loc_Exact
+    end.
+
+  Definition cond_Zopp (b : bool) m := if b then Z.opp m else m.
+
+  Definition SFadd x y :=
+    match x, y with
+    | S754_nan, _ | _, S754_nan => S754_nan
+    | S754_infinity sx, S754_infinity sy =>
+      if Bool.eqb sx sy then x else S754_nan
+    | S754_infinity _, _ => x
+    | _, S754_infinity _ => y
+    | S754_zero sx, S754_zero sy =>
+      if Bool.eqb sx sy then x else
+      S754_zero false
+    | S754_zero _, _ => y
+    | _, S754_zero _ => x
+    | S754_finite sx mx ex, S754_finite sy my ey =>
+      let ez := Z.min ex ey in
+      binary_normalize (Zplus (cond_Zopp sx (Zpos (fst (shl_align mx ex ez)))) (cond_Zopp sy (Zpos (fst (shl_align my ey ez)))))
+        ez false
+    end.
+
+  Definition SFsub x y :=
+    match x, y with
+    | S754_nan, _ | _, S754_nan => S754_nan
+    | S754_infinity sx, S754_infinity sy =>
+      if Bool.eqb sx (negb sy) then x else S754_nan
+    | S754_infinity _, _ => x
+    | _, S754_infinity sy => S754_infinity (negb sy)
+    | S754_zero sx, S754_zero sy =>
+      if Bool.eqb sx (negb sy) then x else
+      S754_zero false
+    | S754_zero _, S754_finite sy my ey => S754_finite (negb sy) my ey
+    | _, S754_zero _ => x
+    | S754_finite sx mx ex, S754_finite sy my ey =>
+      let ez := Z.min ex ey in
+      binary_normalize (Zminus (cond_Zopp sx (Zpos (fst (shl_align mx ex ez)))) (cond_Zopp sy (Zpos (fst (shl_align my ey ez)))))
+        ez false
+    end.
+
+  Definition new_location_even nb_steps k :=
+    if Zeq_bool k 0 then loc_Exact
+    else loc_Inexact (Z.compare (2 * k) nb_steps).
+
+  Definition new_location_odd nb_steps k :=
+    if Zeq_bool k 0 then loc_Exact
+    else
+      loc_Inexact
+      match Z.compare (2 * k + 1) nb_steps with
+      | Lt => Lt
+      | Eq => Lt
+      | Gt => Gt
+      end.
+
+  Definition new_location nb_steps :=
+    if Z.even nb_steps then new_location_even nb_steps else new_location_odd nb_steps.
+
+  Definition SFdiv_core_binary m1 e1 m2 e2 :=
+    let d1 := Zdigits2 m1 in
+    let d2 := Zdigits2 m2 in
+    let e' := Z.min (fexp (d1 + e1 - (d2 + e2))) (e1 - e2) in
+    let s := (e1 - e2 - e')%Z in
+    let m' :=
+      match s with
+      | Zpos _ => Z.shiftl m1 s
+      | Z0 => m1
+      | Zneg _ => Z0
+      end in
+    let '(q, r) := Z.div_eucl m' m2 in
+    (q, e', new_location m2 r).
+
+  Definition SFdiv x y :=
+    match x, y with
+    | S754_nan, _ | _, S754_nan => S754_nan
+    | S754_infinity sx, S754_infinity sy => S754_nan
+    | S754_infinity sx, S754_finite sy _ _ => S754_infinity (xorb sx sy)
+    | S754_finite sx _ _, S754_infinity sy => S754_zero (xorb sx sy)
+    | S754_infinity sx, S754_zero sy => S754_infinity (xorb sx sy)
+    | S754_zero sx, S754_infinity sy => S754_zero (xorb sx sy)
+    | S754_finite sx _ _, S754_zero sy => S754_infinity (xorb sx sy)
+    | S754_zero sx, S754_finite sy _ _ => S754_zero (xorb sx sy)
+    | S754_zero sx, S754_zero sy => S754_nan
+    | S754_finite sx mx ex, S754_finite sy my ey =>
+      let '(mz, ez, lz) := SFdiv_core_binary (Zpos mx) ex (Zpos my) ey in
+      binary_round_aux (xorb sx sy) mz ez lz
+    end.
+
+  Definition SFsqrt_core_binary m e :=
+    let d := Zdigits2 m in
+    let e' := Z.min (fexp (Z.div2 (d + e + 1))) (Z.div2 e) in
+    let s := (e - 2 * e')%Z in
+    let m' :=
+      match s with
+      | Zpos p => Z.shiftl m s
+      | Z0 => m
+      | Zneg _ => Z0
+      end in
+    let (q, r) := Z.sqrtrem m' in
+    let l :=
+      if Zeq_bool r 0 then loc_Exact
+      else loc_Inexact (if Zle_bool r q then Lt else Gt) in
+    (q, e', l).
+
+  Definition SFsqrt x :=
+    match x with
+    | S754_nan => S754_nan
+    | S754_infinity false => x
+    | S754_infinity true => S754_nan
+    | S754_finite true _ _ => S754_nan
+    | S754_zero _ => x
+    | S754_finite sx mx ex =>
+      let '(mz, ez, lz) := SFsqrt_core_binary (Zpos mx) ex in
+      binary_round_aux false mz ez lz
+    end.
+
+  Definition SFnormfr_mantissa f :=
+    match f with
+    | S754_finite _ mx ex =>
+      if Z.eqb ex (-prec) then Npos mx else 0%N
+    | _ => 0%N
+    end.
+
+  Definition SFldexp f e :=
+    match f with
+    | S754_finite sx mx ex => binary_round sx mx (ex+e)
+    | _ => f
+    end.
+
+  Definition SFfrexp f :=
+    match f with
+    | S754_finite sx mx ex =>
+      if (Z.to_pos prec <=? digits2_pos mx)%positive then
+        (S754_finite sx mx (-prec), (ex+prec)%Z)
+      else
+        let d := (prec - Z.pos (digits2_pos mx))%Z in
+        (S754_finite sx (shift_pos (Z.to_pos d) mx) (-prec), (ex+prec-d)%Z)
+    | _ => (f, (-2*emax-prec)%Z)
+    end.
+
+  Definition SFone := binary_round false 1 0.
+
+  Definition SFulp x := SFldexp SFone (fexp (snd (SFfrexp x))).
+
+  Definition SFpred_pos x :=
+    match x with
+    | S754_finite _ mx _ =>
+      let d :=
+        if (mx~0 =? shift_pos (Z.to_pos prec) 1)%positive then
+          SFldexp SFone (fexp (snd (SFfrexp x) - 1))
+        else
+          SFulp x in
+      SFsub x d
+    | _ => x
+    end.
+
+  Definition SFmax_float :=
+    S754_finite false (shift_pos (Z.to_pos prec) 1 - 1) (emax - prec).
+
+  Definition SFsucc x :=
+    match x with
+    | S754_zero _ => SFldexp SFone emin
+    | S754_infinity false => x
+    | S754_infinity true => SFopp SFmax_float
+    | S754_nan => x
+    | S754_finite false _ _ => SFadd x (SFulp x)
+    | S754_finite true _ _ => SFopp (SFpred_pos (SFopp x))
+    end.
+
+  Definition SFpred f := SFopp (SFsucc (SFopp f)).
+End FloatOps.
diff --git a/flocq/Prop/Div_sqrt_error.v b/flocq/Prop/Div_sqrt_error.v
index 79220438..9aa9c508 100644
--- a/flocq/Prop/Div_sqrt_error.v
+++ b/flocq/Prop/Div_sqrt_error.v
@@ -42,9 +42,7 @@ rewrite H; apply generic_format_0.
 rewrite Hx, Hy, <- F2R_plus.
 apply generic_format_F2R.
 intros _.
-case_eq (Fplus fx fy).
-intros mz ez Hz.
-rewrite <- Hz.
+change (F2R _) with (F2R (Fplus fx fy)).
 apply Z.le_trans with (Z.min (Fexp fx) (Fexp fy)).
 rewrite F2R_plus, <- Hx, <- Hy.
 unfold cexp.
@@ -52,7 +50,7 @@ apply Z.le_trans with (1:=Hfexp _).
 apply Zplus_le_reg_l with prec; ring_simplify.
 apply mag_le_bpow with (1 := H).
 now apply Z.min_case.
-rewrite <- Fexp_Fplus, Hz.
+rewrite <- Fexp_Fplus.
 apply Z.le_refl.
 Qed.
 
@@ -100,7 +98,7 @@ apply Rlt_le_trans with (1 := Heps1).
 change 1%R with (bpow 0).
 apply bpow_le.
 generalize (prec_gt_0 prec).
-clear ; omega.
+clear ; lia.
 rewrite Rmult_1_r.
 rewrite Hx2, <- Hx1.
 unfold cexp.
@@ -193,7 +191,7 @@ now apply IZR_lt.
 rewrite <- Rmult_assoc, Rinv_r, Rmult_1_l.
 apply Rle_trans with (bpow (-1)).
 apply bpow_le.
-omega.
+lia.
 replace (2 * (-1 + 5 / 4))%R with (/2)%R by field.
 apply Rinv_le.
 now apply IZR_lt.
@@ -280,11 +278,11 @@ apply Rle_not_lt.
 rewrite <- Hr1.
 apply abs_round_ge_generic...
 apply generic_format_bpow.
-unfold FLX_exp; omega.
+unfold FLX_exp; lia.
 apply Es.
 apply Rlt_le_trans with (1:=H).
 apply bpow_le.
-omega.
+lia.
 now apply Rlt_le.
 Qed.
 
@@ -319,7 +317,7 @@ rewrite <- bpow_plus; apply bpow_le; unfold e; set (mxm1 := (_ - 1)%Z).
 replace (_ * _)%Z with (2 * (mxm1 / 2) + mxm1 mod 2 - mxm1 mod 2)%Z by ring.
 rewrite <- Z.div_mod; [|now simpl].
 apply (Zplus_le_reg_r _ _ (mxm1 mod 2 - mag beta x)%Z).
-unfold mxm1; destruct (Z.mod_bound_or (mag beta x - 1) 2); omega.
+unfold mxm1; destruct (Z.mod_bound_or (mag beta x - 1) 2); lia.
 Qed.
 
 Notation u_ro := (u_ro beta prec).
@@ -346,7 +344,7 @@ assert (Hulp1p2eps : (ulp beta (FLX_exp prec) (1 + 2 * u_ro) = 2 * u_ro)%R).
   rewrite succ_FLX_1, mag_1, bpow_1, <- H2eps; simpl.
   apply (Rlt_le_trans _ 2); [apply Rplus_lt_compat_l|].
   { unfold u_ro; rewrite <-Rmult_assoc, Rinv_r, Rmult_1_l; [|lra].
-    change R1 with (bpow 0); apply bpow_lt; omega. }
+    change R1 with (bpow 0); apply bpow_lt; lia. }
   apply IZR_le, Zle_bool_imp_le, radix_prop. }
 assert (Hsucc1p2eps :
           (succ beta (FLX_exp prec) (1 + 2 * u_ro) = 1 + 4 * u_ro)%R).
@@ -383,7 +381,7 @@ ring_simplify; apply Rsqr_incr_0_var.
   apply Rmult_le_pos; [|now apply pow_le].
   assert (Heps_le_half : (u_ro <= 1 / 2)%R).
   { unfold u_ro, Rdiv; rewrite Rmult_comm; apply Rmult_le_compat_r; [lra|].
-    change 1%R with (bpow 0); apply bpow_le; omega. }
+    change 1%R with (bpow 0); apply bpow_le; lia. }
   apply (Rle_trans _ (-8 * u_ro + 4)); [lra|].
   apply Rplus_le_compat_r, Rmult_le_compat_r; [apply Pu_ro|].
   now assert (H : (0 <= u_ro ^ 2)%R); [apply pow2_ge_0|lra]. }
@@ -447,13 +445,13 @@ destruct (sqrt_error_N_FLX_aux2 _ Fmu HmuGe1) as [Hmu'|[Hmu'|Hmu']].
   { rewrite Rminus_diag_eq, Rabs_R0; [|now simpl].
     now apply Rmult_le_pos; [|apply Rabs_pos]. }
   apply generic_format_bpow'; [now apply FLX_exp_valid|].
-  unfold FLX_exp; omega. }
+  unfold FLX_exp; lia. }
 { assert (Hsqrtmu : (1 <= sqrt mu < 1 + u_ro)%R); [rewrite Hmu'; split|].
   { rewrite <- sqrt_1 at 1; apply sqrt_le_1_alt; lra. }
   { rewrite <- sqrt_square; [|lra]; apply sqrt_lt_1_alt; split; [lra|].
     ring_simplify; assert (0 < u_ro ^ 2)%R; [apply pow_lt|]; lra. }
   assert (Fbpowe : generic_format beta (FLX_exp prec) (bpow e)).
-  { apply generic_format_bpow; unfold FLX_exp; omega. }
+  { apply generic_format_bpow; unfold FLX_exp; lia. }
   assert (Hrt : rt = bpow e :> R).
   { unfold rt; fold t; rewrite Ht; simpl; apply Rle_antisym.
     { apply round_N_le_midp; [now apply FLX_exp_valid|exact Fbpowe|].
@@ -495,7 +493,7 @@ assert (Hulpt : (ulp beta (FLX_exp prec) t = 2 * u_ro * bpow e)%R).
       { apply sqrt_lt_1_alt; split; [lra|].
         apply (Rlt_le_trans _ _ _ HmuLtsqradix); right.
         now unfold bpow, Z.pow_pos; simpl; rewrite Zmult_1_r, mult_IZR. }
-      apply IZR_le, (Z.le_trans _ 2), Zle_bool_imp_le, radix_prop; omega. }
+      apply IZR_le, (Z.le_trans _ 2), Zle_bool_imp_le, radix_prop; lia. }
     rewrite Hmagt; ring. }
   rewrite Ht; apply Rmult_lt_0_compat; [|now apply bpow_gt_0].
   now apply (Rlt_le_trans _ 1); [lra|rewrite <- sqrt_1; apply sqrt_le_1_alt]. }
@@ -656,7 +654,7 @@ apply Fourier_util.Rle_mult_inv_pos; assumption.
 case (Zle_lt_or_eq 0 n); try exact H.
 clear H; intros H.
 case (Zle_lt_or_eq 1 n).
-omega.
+lia.
 clear H; intros H.
 set (ex := cexp beta fexp x).
 set (ey := cexp beta fexp y).
@@ -715,7 +713,7 @@ rewrite Rinv_l, Rmult_1_r, Rmult_1_l.
 assert (mag beta x < mag beta y)%Z.
 case (Zle_or_lt (mag beta y) (mag beta x)); try easy.
 intros J; apply monotone_exp in J; clear -J Hexy.
-unfold ex, ey, cexp in Hexy; omega.
+unfold ex, ey, cexp in Hexy; lia.
 left; apply lt_mag with beta; easy.
 (* n = 1 -> Sterbenz + rnd_small *)
 intros Hn'; fold n; rewrite <- Hn'.
diff --git a/flocq/Prop/Double_rounding.v b/flocq/Prop/Double_rounding.v
index 055409bb..3e942fe0 100644
--- a/flocq/Prop/Double_rounding.v
+++ b/flocq/Prop/Double_rounding.v
@@ -122,7 +122,7 @@ destruct (Req_dec x'' 0) as [Zx''|Nzx''].
   apply (Rle_lt_trans _ _ _ Hr1).
   apply Rmult_lt_compat_l; [lra|].
   apply bpow_lt.
-  omega.
+  lia.
 - (* x'' <> 0 *)
   assert (Lx'' : mag x'' = mag x :> Z).
   { apply Zle_antisym.
@@ -203,7 +203,7 @@ destruct (Req_dec x' 0) as [Zx'|Nzx'].
   replace (2 * (/ 2 * _)) with (bpow (fexp1 (mag x) - mag x)) by field.
   apply Rle_trans with 1; [|lra].
   change 1 with (bpow 0); apply bpow_le.
-  omega.
+  lia.
 - (* x' <> 0 *)
   assert (Px' : 0 < x').
   { assert (0 <= x'); [|lra].
@@ -314,10 +314,10 @@ Proof.
 intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hf1 Hx Hx'.
 destruct (Zle_or_lt (fexp1 (mag x)) (fexp2 (mag x))) as [Hf2'|Hf2'].
 - (* fexp1 (mag x) <= fexp2 (mag x) *)
-  assert (Hf2'' : (fexp2 (mag x) = fexp1 (mag x) :> Z)%Z); [omega|].
+  assert (Hf2'' : (fexp2 (mag x) = fexp1 (mag x) :> Z)%Z) by lia.
   now apply round_round_lt_mid_same_place.
 - (* fexp2 (mag x) < fexp1 (mag x) *)
-  assert (Hf2'' : (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z); [omega|].
+  assert (Hf2'' : (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z) by lia.
   generalize (Hx' Hf2''); intro Hx''.
   now apply round_round_lt_mid_further_place.
 Qed.
@@ -380,7 +380,7 @@ destruct (Req_dec x'' 0) as [Zx''|Nzx''].
   apply (Rle_lt_trans _ _ _ Hr1).
   apply Rmult_lt_compat_l; [lra|].
   apply bpow_lt.
-  omega.
+  lia.
 - (* x'' <> 0 *)
   assert (Lx'' : mag x'' = mag x :> Z).
   { apply Zle_antisym.
@@ -460,11 +460,11 @@ assert (Hx''pow : x'' = bpow (mag x)).
   unfold x'', round, F2R, scaled_mantissa, cexp; simpl.
   apply (Rmult_le_reg_r (bpow (- fexp2 (mag x)))); [now apply bpow_gt_0|].
   bpow_simplify.
-  rewrite <- (IZR_Zpower _ (_ - _)); [|omega].
+  rewrite <- (IZR_Zpower _ (_ - _)); [|lia].
   apply IZR_le.
   apply Zlt_succ_le; unfold Z.succ.
   apply lt_IZR.
-  rewrite plus_IZR; rewrite IZR_Zpower; [|omega].
+  rewrite plus_IZR; rewrite IZR_Zpower; [|lia].
   apply (Rmult_lt_reg_r (bpow (fexp2 (mag x)))); [now apply bpow_gt_0|].
   rewrite Rmult_plus_distr_r; rewrite Rmult_1_l.
   bpow_simplify.
@@ -482,12 +482,12 @@ assert (Hr : Rabs (x - x'') < / 2 * ulp beta fexp1 x).
   - apply Rmult_lt_compat_l; [lra|].
     rewrite 2!ulp_neq_0; try now apply Rgt_not_eq.
     unfold cexp; apply bpow_lt.
-    omega. }
+    lia. }
 unfold round, F2R, scaled_mantissa, cexp; simpl.
 assert (Hf : (0 <= mag x - fexp1 (mag x''))%Z).
 { rewrite Hx''pow.
   rewrite mag_bpow.
-  assert (fexp1 (mag x + 1) <= mag x)%Z; [|omega].
+  assert (fexp1 (mag x + 1) <= mag x)%Z; [|lia].
   destruct (Zle_or_lt (mag x) (fexp1 (mag x))) as [Hle|Hlt];
     [|now apply Vfexp1].
   assert (H : (mag x = fexp1 (mag x) :> Z)%Z);
@@ -497,9 +497,9 @@ assert (Hf : (0 <= mag x - fexp1 (mag x''))%Z).
 rewrite (Znearest_imp _ _ (beta ^ (mag x - fexp1 (mag x'')))%Z).
 - rewrite (Znearest_imp _ _ (beta ^ (mag x - fexp1 (mag x)))%Z).
   + rewrite IZR_Zpower; [|exact Hf].
-    rewrite IZR_Zpower; [|omega].
+    rewrite IZR_Zpower; [|lia].
     now bpow_simplify.
-  + rewrite IZR_Zpower; [|omega].
+  + rewrite IZR_Zpower; [|lia].
     apply (Rmult_lt_reg_r (bpow (fexp1 (mag x)))); [now apply bpow_gt_0|].
     rewrite <- (Rabs_right (bpow (fexp1 _))) at 1;
       [|now apply Rle_ge; apply bpow_ge_0].
@@ -588,10 +588,10 @@ Proof.
 intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hf1 Hx Hx'.
 destruct (Zle_or_lt (fexp1 (mag x)) (fexp2 (mag x))) as [Hf2'|Hf2'].
 - (* fexp1 (mag x) <= fexp2 (mag x) *)
-  assert (Hf2'' : (fexp2 (mag x) = fexp1 (mag x) :> Z)%Z); [omega|].
+  assert (Hf2'' : (fexp2 (mag x) = fexp1 (mag x) :> Z)%Z) by lia.
   now apply round_round_gt_mid_same_place.
 - (* fexp2 (mag x) < fexp1 (mag x) *)
-  assert (Hf2'' : (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z); [omega|].
+  assert (Hf2'' : (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z) by lia.
   generalize (Hx' Hf2''); intro Hx''.
   now apply round_round_gt_mid_further_place.
 Qed.
@@ -606,7 +606,7 @@ Lemma mag_mult_disj :
 Proof.
 intros x y Zx Zy.
 destruct (mag_mult beta x y Zx Zy).
-omega.
+lia.
 Qed.
 
 Definition round_round_mult_hyp fexp1 fexp2 :=
@@ -691,7 +691,7 @@ intros Hprec x y Fx Fy.
 apply round_round_mult;
   [|now apply generic_format_FLX|now apply generic_format_FLX].
 unfold round_round_mult_hyp; split; intros ex ey; unfold FLX_exp;
-omega.
+lia.
 Qed.
 
 End Double_round_mult_FLX.
@@ -721,7 +721,7 @@ generalize (Zmax_spec (ex + ey - prec') emin');
 generalize (Zmax_spec (ex + ey - 1 - prec') emin');
 generalize (Zmax_spec (ex - prec) emin);
 generalize (Zmax_spec (ey - prec) emin);
-omega.
+lia.
 Qed.
 
 End Double_round_mult_FLT.
@@ -753,7 +753,7 @@ destruct (Z.ltb_spec (ex + ey - prec') emin');
 destruct (Z.ltb_spec (ex - prec) emin);
 destruct (Z.ltb_spec (ey - prec) emin);
 destruct (Z.ltb_spec (ex + ey - 1 - prec') emin');
-omega.
+lia.
 Qed.
 
 End Double_round_mult_FTZ.
@@ -770,7 +770,7 @@ Lemma mag_plus_disj :
 Proof.
 intros x y Py Hxy.
 destruct (mag_plus beta x y Py Hxy).
-omega.
+lia.
 Qed.
 
 Lemma mag_plus_separated :
@@ -798,10 +798,10 @@ Lemma mag_minus_disj :
    \/ (mag (x - y) = (mag x - 1)%Z :> Z)).
 Proof.
 intros x y Px Py Hln.
-assert (Hxy : y < x); [now apply (lt_mag beta); [ |omega]|].
+assert (Hxy : y < x); [now apply (lt_mag beta); [ |lia]|].
 generalize (mag_minus beta x y Py Hxy); intro Hln2.
 generalize (mag_minus_lb beta x y Px Py Hln); intro Hln3.
-omega.
+lia.
 Qed.
 
 Lemma mag_minus_separated :
@@ -831,7 +831,7 @@ split.
     apply succ_le_lt; [apply Vfexp|idtac|exact Fx|assumption].
     apply (generic_format_bpow beta fexp (mag x - 1)).
     replace (_ + _)%Z with (mag x : Z) by ring.
-    assert (fexp (mag x) < mag x)%Z; [|omega].
+    assert (fexp (mag x) < mag x)%Z; [|lia].
     now apply mag_generic_gt; [|now apply Rgt_not_eq|].
 - rewrite Rabs_right.
   + apply Rlt_trans with x.
@@ -884,7 +884,7 @@ destruct (Req_dec x 0) as [Zx|Nzx].
       rewrite Rmult_plus_distr_r.
       rewrite <- Fx.
       rewrite mult_IZR.
-      rewrite IZR_Zpower; [|omega].
+      rewrite IZR_Zpower; [|lia].
       bpow_simplify.
       now rewrite <- Fy. }
     apply generic_format_F2R' with (f := fxy); [now rewrite Hxy|].
@@ -904,7 +904,7 @@ intros fexp1 fexp2 x y Hlnx Hlny Fx Fy.
 destruct (Z.le_gt_cases (fexp1 (mag x)) (fexp1 (mag y))) as [Hle|Hgt].
 - now apply (round_round_plus_aux0_aux_aux fexp1).
 - rewrite Rplus_comm in Hlnx, Hlny |- *.
-  now apply (round_round_plus_aux0_aux_aux fexp1); [omega| | | |].
+  now apply (round_round_plus_aux0_aux_aux fexp1); [lia| | | |].
 Qed.
 
 (* fexp1 (mag x) - 1 <= mag y :
@@ -927,20 +927,20 @@ destruct (Z.le_gt_cases (mag y) (fexp1 (mag x))) as [Hle|Hgt].
   [now apply (mag_plus_separated fexp1)|].
   apply (round_round_plus_aux0_aux fexp1);
     [| |assumption|assumption]; rewrite Lxy.
-  + now apply Hexp4; omega.
-  + now apply Hexp3; omega.
+  + now apply Hexp4; lia.
+  + now apply Hexp3; lia.
 - (* fexp1 (mag x) < mag y *)
   apply (round_round_plus_aux0_aux fexp1); [| |assumption|assumption].
   destruct (mag_plus_disj x y Py Hyx) as [Lxy|Lxy]; rewrite Lxy.
-  + now apply Hexp4; omega.
+  + now apply Hexp4; lia.
   + apply Hexp2; apply (mag_le beta y x Py) in Hyx.
     replace (_ - _)%Z with (mag x : Z) by ring.
-    omega.
+    lia.
   + destruct (mag_plus_disj x y Py Hyx) as [Lxy|Lxy]; rewrite Lxy.
-    * now apply Hexp3; omega.
+    * now apply Hexp3; lia.
     * apply Hexp2.
       replace (_ - _)%Z with (mag x : Z) by ring.
-      omega.
+      lia.
 Qed.
 
 Lemma round_round_plus_aux1_aux :
@@ -983,7 +983,7 @@ assert (UB : y * bpow (- fexp (mag x)) < / IZR (beta ^ k)).
     + bpow_simplify.
       rewrite bpow_opp.
       destruct k.
-      * omega.
+      * lia.
       * simpl; unfold Raux.bpow, Z.pow_pos.
         now apply Rle_refl.
       * casetype False; apply (Z.lt_irrefl 0).
@@ -1003,7 +1003,7 @@ rewrite (Zfloor_imp mx).
     apply (Rlt_le_trans _ _ _ UB).
     rewrite bpow_opp.
     apply Rinv_le; [now apply bpow_gt_0|].
-    now rewrite IZR_Zpower; [right|omega]. }
+    now rewrite IZR_Zpower; [right|lia]. }
 split.
 - rewrite <- Rplus_0_r at 1; apply Rplus_le_compat_l.
   now apply Rlt_le.
@@ -1014,7 +1014,7 @@ split.
   apply Rlt_trans with (bpow (mag y)).
   + rewrite <- Rabs_right at 1; [|now apply Rle_ge; apply Rlt_le].
     apply bpow_mag_gt.
-  + apply bpow_lt; omega.
+  + apply bpow_lt; lia.
 Qed.
 
 (* mag y <= fexp1 (mag x) - 2 : round_round_lt_mid applies. *)
@@ -1034,18 +1034,18 @@ assert (Hbeta : (2 <= beta)%Z).
   now apply Zle_bool_imp_le. }
 intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Px Py Hly Fx.
 assert (Lxy : mag (x + y) = mag x :> Z);
-  [now apply (mag_plus_separated fexp1); [|apply Rlt_le| |omega]|].
+  [now apply (mag_plus_separated fexp1); [|apply Rlt_le| |lia]|].
 destruct Hexp as (_,(_,(_,Hexp4))).
 assert (Hf2 : (fexp2 (mag x) <= fexp1 (mag x))%Z);
-  [now apply Hexp4; omega|].
+  [now apply Hexp4; lia|].
 assert (Bpow2 : bpow (- 2) <= / 2 * / 2).
 { replace (/2 * /2) with (/4) by field.
   rewrite (bpow_opp _ 2).
   apply Rinv_le; [lra|].
   apply (IZR_le (2 * 2) (beta * (beta * 1))).
   rewrite Zmult_1_r.
-  now apply Zmult_le_compat; omega. }
-assert (P2 : (0 < 2)%Z) by omega.
+  now apply Zmult_le_compat; lia. }
+assert (P2 : (0 < 2)%Z) by lia.
 unfold round_round_eq.
 apply round_round_lt_mid.
 - exact Vfexp1.
@@ -1053,7 +1053,7 @@ apply round_round_lt_mid.
 - lra.
 - now rewrite Lxy.
 - rewrite Lxy.
-  assert (fexp1 (mag x) < mag x)%Z; [|omega].
+  assert (fexp1 (mag x) < mag x)%Z; [|lia].
   now apply mag_generic_gt; [|apply Rgt_not_eq|].
 - unfold midp.
   apply (Rplus_lt_reg_r (- round beta fexp1 Zfloor (x + y))).
@@ -1088,10 +1088,10 @@ apply round_round_lt_mid.
   replace (_ - _) with (- (/ 2)) by lra.
   apply Ropp_le_contravar.
   { apply Rle_trans with (bpow (- 1)).
-    - apply bpow_le; omega.
+    - apply bpow_le; lia.
     - unfold Raux.bpow, Z.pow_pos; simpl.
       apply Rinv_le; [lra|].
-      apply IZR_le; omega. }
+      apply IZR_le; lia. }
 Qed.
 
 (* round_round_plus_aux{0,1} together *)
@@ -1115,7 +1115,7 @@ destruct (Zle_or_lt (mag y) (fexp1 (mag x) - 2)) as [Hly|Hly].
   rewrite (round_generic beta fexp2).
   + reflexivity.
   + now apply valid_rnd_N.
-  + assert (Hf1 : (fexp1 (mag x) - 1 <= mag y)%Z); [omega|].
+  + assert (Hf1 : (fexp1 (mag x) - 1 <= mag y)%Z) by lia.
     now apply (round_round_plus_aux0 fexp1).
 Qed.
 
@@ -1140,7 +1140,7 @@ destruct (Req_dec x 0) as [Zx|Nzx].
   + reflexivity.
   + now apply valid_rnd_N.
   + apply (generic_inclusion_mag beta fexp1).
-    now intros _; apply Hexp4; omega.
+    now intros _; apply Hexp4; lia.
     exact Fy.
 - (* x <> 0 *)
   destruct (Req_dec y 0) as [Zy|Nzy].
@@ -1151,7 +1151,7 @@ destruct (Req_dec x 0) as [Zx|Nzx].
     * reflexivity.
     * now apply valid_rnd_N.
     * apply (generic_inclusion_mag beta fexp1).
-      now intros _; apply Hexp4; omega.
+      now intros _; apply Hexp4; lia.
       exact Fx.
   + (* y <> 0 *)
     assert (Px : 0 < x); [lra|].
@@ -1199,21 +1199,21 @@ assert (Lyx : (mag y <= mag x)%Z);
 destruct (Z.lt_ge_cases (mag x - 2) (mag y)) as [Hlt|Hge].
 - (* mag x - 2 < mag y *)
   assert (Hor : (mag y = mag x :> Z)
-                \/ (mag y = mag x - 1 :> Z)%Z); [omega|].
+                \/ (mag y = mag x - 1 :> Z)%Z) by lia.
   destruct Hor as [Heq|Heqm1].
   + (* mag y = mag x *)
     apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy].
     * apply Hexp4.
-      apply Z.le_trans with (mag (x - y)); [omega|].
+      apply Z.le_trans with (mag (x - y)); [lia|].
       now apply mag_minus.
     * rewrite Heq.
       apply Hexp4.
-      apply Z.le_trans with (mag (x - y)); [omega|].
+      apply Z.le_trans with (mag (x - y)); [lia|].
       now apply mag_minus.
   + (* mag y = mag x - 1 *)
     apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy].
     * apply Hexp4.
-      apply Z.le_trans with (mag (x - y)); [omega|].
+      apply Z.le_trans with (mag (x - y)); [lia|].
       now apply mag_minus.
     * rewrite Heqm1.
       apply Hexp4.
@@ -1224,7 +1224,7 @@ destruct (Z.lt_ge_cases (mag x - 2) (mag y)) as [Hlt|Hge].
   + (* mag (x - y) = mag x *)
     apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy].
     * apply Hexp4.
-      omega.
+      lia.
     * now rewrite Lxmy; apply Hexp3.
   + (* mag (x - y) = mag x - 1 *)
     apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy];
@@ -1261,8 +1261,8 @@ assert (Hfy : (fexp1 (mag y) < mag y)%Z);
   [now apply mag_generic_gt; [|apply Rgt_not_eq|]|].
 apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy].
 - apply Z.le_trans with (fexp1 (mag (x - y))).
-  + apply Hexp4; omega.
-  + omega.
+  + apply Hexp4; lia.
+  + lia.
 - now apply Hexp3.
 Qed.
 
@@ -1289,7 +1289,7 @@ assert (Hfy : (fexp (mag y) < mag y)%Z);
 destruct (Rlt_or_le (bpow (mag x - 1)) x) as [Hx|Hx].
 - (* bpow (mag x - 1) < x *)
   assert (Lxy : mag (x - y) = mag x :> Z);
-    [now apply (mag_minus_separated fexp); [| | | | | |omega]|].
+    [now apply (mag_minus_separated fexp); [| | | | | |lia]|].
   assert (Rxy : round beta fexp Zceil (x - y) = x).
   { unfold round, F2R, scaled_mantissa, cexp; simpl.
     rewrite Lxy.
@@ -1311,7 +1311,7 @@ destruct (Rlt_or_le (bpow (mag x - 1)) x) as [Hx|Hx].
       + rewrite <- Rabs_right at 1; [|now apply Rle_ge; apply Rlt_le].
         apply bpow_mag_gt.
       + apply bpow_le.
-        omega.
+        lia.
     - rewrite <- (Rplus_0_r (IZR _)) at 2.
       apply Rplus_le_compat_l.
       rewrite <- Ropp_0; apply Ropp_le_contravar.
@@ -1334,9 +1334,9 @@ destruct (Rlt_or_le (bpow (mag x - 1)) x) as [Hx|Hx].
         now intro Hx'; rewrite Hx' in Hxy; apply (Rlt_irrefl y).
       + rewrite Rabs_right; lra.
     - apply (mag_minus_lb beta x y Px Py).
-      omega. }
+      lia. }
   assert (Hfx1 : (fexp (mag x - 1) < mag x - 1)%Z);
-    [now apply (valid_exp_large fexp (mag y)); [|omega]|].
+    [now apply (valid_exp_large fexp (mag y)); [|lia]|].
   assert (Rxy : round beta fexp Zceil (x - y) <= x).
   { rewrite Xpow at 2.
     unfold round, F2R, scaled_mantissa, cexp; simpl.
@@ -1344,10 +1344,10 @@ destruct (Rlt_or_le (bpow (mag x - 1)) x) as [Hx|Hx].
     apply (Rmult_le_reg_r (bpow (- fexp (mag x - 1)%Z)));
       [now apply bpow_gt_0|].
     bpow_simplify.
-    rewrite <- (IZR_Zpower beta (_ - _ - _)); [|omega].
+    rewrite <- (IZR_Zpower beta (_ - _ - _)); [|lia].
     apply IZR_le.
     apply Zceil_glb.
-    rewrite IZR_Zpower; [|omega].
+    rewrite IZR_Zpower; [|lia].
     rewrite Xpow at 1.
     rewrite Rmult_minus_distr_r.
     bpow_simplify.
@@ -1383,7 +1383,7 @@ intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Py Hxy Hly Hly' Fx Fy.
 assert (Px := Rlt_trans 0 y x Py Hxy).
 destruct Hexp as (_,(_,(_,Hexp4))).
 assert (Hf2 : (fexp2 (mag x) <= fexp1 (mag x))%Z);
-  [now apply Hexp4; omega|].
+  [now apply Hexp4; lia|].
 assert (Hfx : (fexp1 (mag x) < mag x)%Z);
   [now apply mag_generic_gt; [|apply Rgt_not_eq|]|].
 assert (Bpow2 : bpow (- 2) <= / 2 * / 2).
@@ -1392,7 +1392,7 @@ assert (Bpow2 : bpow (- 2) <= / 2 * / 2).
   apply Rinv_le; [lra|].
   apply (IZR_le (2 * 2) (beta * (beta * 1))).
   rewrite Zmult_1_r.
-  now apply Zmult_le_compat; omega. }
+  now apply Zmult_le_compat; lia. }
 assert (Ly : y < bpow (mag y)).
 { apply Rabs_lt_inv.
   apply bpow_mag_gt. }
@@ -1401,19 +1401,19 @@ apply round_round_gt_mid.
 - exact Vfexp1.
 - exact Vfexp2.
 - lra.
-- apply Hexp4; omega.
-- assert (fexp1 (mag (x - y)) < mag (x - y))%Z; [|omega].
+- apply Hexp4; lia.
+- assert (fexp1 (mag (x - y)) < mag (x - y))%Z; [|lia].
   apply (valid_exp_large fexp1 (mag x - 1)).
-  + apply (valid_exp_large fexp1 (mag y)); [|omega].
+  + apply (valid_exp_large fexp1 (mag y)); [|lia].
     now apply mag_generic_gt; [|apply Rgt_not_eq|].
-  + now apply mag_minus_lb; [| |omega].
+  + now apply mag_minus_lb; [| |lia].
 - unfold midp'.
   apply (Rplus_lt_reg_r (/ 2 * ulp beta fexp1 (x - y) - (x - y))).
   ring_simplify.
   replace (_ + _) with (round beta fexp1 Zceil (x - y) - (x - y)) by ring.
   apply Rlt_le_trans with (bpow (fexp1 (mag (x - y)) - 2)).
   + apply Rle_lt_trans with y;
-    [now apply round_round_minus_aux2_aux; try assumption; omega|].
+    [now apply round_round_minus_aux2_aux; try assumption; lia|].
     apply (Rlt_le_trans _ _ _ Ly).
     now apply bpow_le.
   + rewrite ulp_neq_0;[idtac|now apply sym_not_eq, Rlt_not_eq, Rgt_minus].
@@ -1428,7 +1428,7 @@ apply round_round_gt_mid.
       rewrite Zmult_1_r; apply Rinv_le.
       lra.
       now apply IZR_le.
-    * apply bpow_le; omega.
+    * apply bpow_le; lia.
 - intro Hf2'.
   unfold midp'.
   apply (Rplus_lt_reg_r (/ 2 * ulp beta fexp1 (x - y) - (x - y)
@@ -1436,7 +1436,7 @@ apply round_round_gt_mid.
   ring_simplify.
   replace (_ + _) with (round beta fexp1 Zceil (x - y) - (x - y)) by ring.
   apply Rle_lt_trans with y;
-    [now apply round_round_minus_aux2_aux; try assumption; omega|].
+    [now apply round_round_minus_aux2_aux; try assumption; lia|].
   apply (Rlt_le_trans _ _ _ Ly).
   apply Rle_trans with (bpow (fexp1 (mag (x - y)) - 2));
     [now apply bpow_le|].
@@ -1501,12 +1501,12 @@ destruct (Req_dec y x) as [Hy|Hy].
       { rewrite (round_generic beta fexp2).
         - reflexivity.
         - now apply valid_rnd_N.
-        - assert (Hf1 : (fexp1 (mag (x - y)) - 1 <= mag y)%Z); [omega|].
+        - assert (Hf1 : (fexp1 (mag (x - y)) - 1 <= mag y)%Z) by lia.
           now apply (round_round_minus_aux1 fexp1). }
   + rewrite (round_generic beta fexp2).
     * reflexivity.
     * now apply valid_rnd_N.
-    * assert (Hf1 : (fexp1 (mag x) - 1 <= mag y)%Z); [omega|].
+    * assert (Hf1 : (fexp1 (mag x) - 1 <= mag y)%Z) by lia.
       now apply (round_round_minus_aux0 fexp1).
 Qed.
 
@@ -1532,7 +1532,7 @@ destruct (Req_dec x 0) as [Zx|Nzx].
   * now apply valid_rnd_N.
   * apply (generic_inclusion_mag beta fexp1).
     destruct Hexp as (_,(_,(_,Hexp4))).
-    now intros _; apply Hexp4; omega.
+    now intros _; apply Hexp4; lia.
     exact Fy.
 - (* x <> 0 *)
   destruct (Req_dec y 0) as [Zy|Nzy].
@@ -1543,7 +1543,7 @@ destruct (Req_dec x 0) as [Zx|Nzx].
     * now apply valid_rnd_N.
     * apply (generic_inclusion_mag beta fexp1).
       destruct Hexp as (_,(_,(_,Hexp4))).
-      now intros _; apply Hexp4; omega.
+      now intros _; apply Hexp4; lia.
       exact Fx.
   + (* y <> 0 *)
     assert (Px : 0 < x); [lra|].
@@ -1626,9 +1626,9 @@ Proof.
 intros Hprec.
 unfold FLX_exp.
 unfold round_round_plus_hyp; split; [|split; [|split]];
-intros ex ey; try omega.
+intros ex ey; try lia.
 unfold Prec_gt_0 in prec_gt_0_.
-omega.
+lia.
 Qed.
 
 Theorem round_round_plus_FLX :
@@ -1683,19 +1683,19 @@ unfold round_round_plus_hyp; split; [|split; [|split]]; intros ex ey.
 - generalize (Zmax_spec (ex + 1 - prec) emin).
   generalize (Zmax_spec (ex - prec') emin').
   generalize (Zmax_spec (ey - prec) emin).
-  omega.
+  lia.
 - generalize (Zmax_spec (ex - 1 - prec) emin).
   generalize (Zmax_spec (ex - prec') emin').
   generalize (Zmax_spec (ey - prec) emin).
-  omega.
+  lia.
 - generalize (Zmax_spec (ex - prec) emin).
   generalize (Zmax_spec (ex - prec') emin').
   generalize (Zmax_spec (ey - prec) emin).
-  omega.
+  lia.
 - unfold Prec_gt_0 in prec_gt_0_.
   generalize (Zmax_spec (ex - prec') emin').
   generalize (Zmax_spec (ey - prec) emin).
-  omega.
+  lia.
 Qed.
 
 Theorem round_round_plus_FLT :
@@ -1753,18 +1753,18 @@ unfold round_round_plus_hyp; split; [|split; [|split]]; intros ex ey.
 - destruct (Z.ltb_spec (ex + 1 - prec) emin);
   destruct (Z.ltb_spec (ex - prec') emin');
   destruct (Z.ltb_spec (ey - prec) emin);
-  omega.
+  lia.
 - destruct (Z.ltb_spec (ex - 1 - prec) emin);
   destruct (Z.ltb_spec (ex - prec') emin');
   destruct (Z.ltb_spec (ey - prec) emin);
-  omega.
+  lia.
 - destruct (Z.ltb_spec (ex - prec) emin);
   destruct (Z.ltb_spec (ex - prec') emin');
   destruct (Z.ltb_spec (ey - prec) emin);
-  omega.
+  lia.
 - destruct (Z.ltb_spec (ex - prec') emin');
   destruct (Z.ltb_spec (ey - prec) emin);
-  omega.
+  lia.
 Qed.
 
 Theorem round_round_plus_FTZ :
@@ -1832,20 +1832,20 @@ destruct (Z.le_gt_cases (mag y) (fexp1 (mag x))) as [Hle|Hgt].
   [now apply (mag_plus_separated fexp1)|].
   apply (round_round_plus_aux0_aux fexp1);
     [| |assumption|assumption]; rewrite Lxy.
-  + now apply Hexp4; omega.
-  + now apply Hexp3; omega.
+  + now apply Hexp4; lia.
+  + now apply Hexp3; lia.
 - (* fexp1 (mag x) < mag y *)
   apply (round_round_plus_aux0_aux fexp1); [| |assumption|assumption].
   destruct (mag_plus_disj x y Py Hyx) as [Lxy|Lxy]; rewrite Lxy.
-  + now apply Hexp4; omega.
+  + now apply Hexp4; lia.
   + apply Hexp2; apply (mag_le beta y x Py) in Hyx.
     replace (_ - _)%Z with (mag x : Z) by ring.
-    omega.
+    lia.
   + destruct (mag_plus_disj x y Py Hyx) as [Lxy|Lxy]; rewrite Lxy.
-    * now apply Hexp3; omega.
+    * now apply Hexp3; lia.
     * apply Hexp2.
       replace (_ - _)%Z with (mag x : Z) by ring.
-      omega.
+      lia.
 Qed.
 
 (* mag y <= fexp1 (mag x) - 1 : round_round_lt_mid applies. *)
@@ -1863,16 +1863,16 @@ Lemma round_round_plus_radix_ge_3_aux1 :
 Proof.
 intros Hbeta fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Px Py Hly Fx.
 assert (Lxy : mag (x + y) = mag x :> Z);
-  [now apply (mag_plus_separated fexp1); [|apply Rlt_le| |omega]|].
+  [now apply (mag_plus_separated fexp1); [|apply Rlt_le| |lia]|].
 destruct Hexp as (_,(_,(_,Hexp4))).
 assert (Hf2 : (fexp2 (mag x) <= fexp1 (mag x))%Z);
-  [now apply Hexp4; omega|].
+  [now apply Hexp4; lia|].
 assert (Bpow3 : bpow (- 1) <= / 3).
 { unfold Raux.bpow, Z.pow_pos; simpl.
   rewrite Zmult_1_r.
   apply Rinv_le; [lra|].
   now apply IZR_le. }
-assert (P1 : (0 < 1)%Z) by omega.
+assert (P1 : (0 < 1)%Z) by lia.
 unfold round_round_eq.
 apply round_round_lt_mid.
 - exact Vfexp1.
@@ -1880,7 +1880,7 @@ apply round_round_lt_mid.
 - lra.
 - now rewrite Lxy.
 - rewrite Lxy.
-  assert (fexp1 (mag x) < mag x)%Z; [|omega].
+  assert (fexp1 (mag x) < mag x)%Z; [|lia].
   now apply mag_generic_gt; [|apply Rgt_not_eq|].
 - unfold midp.
   apply (Rplus_lt_reg_r (- round beta fexp1 Zfloor (x + y))).
@@ -1914,7 +1914,7 @@ apply round_round_lt_mid.
   apply (Rplus_le_reg_r (- 1)); ring_simplify.
   replace (_ - _) with (- (/ 3)) by lra.
   apply Ropp_le_contravar.
-  now apply Rle_trans with (bpow (- 1)); [apply bpow_le; omega|].
+  now apply Rle_trans with (bpow (- 1)); [apply bpow_le; lia|].
 Qed.
 
 (* round_round_plus_radix_ge_3_aux{0,1} together *)
@@ -1940,7 +1940,7 @@ destruct (Zle_or_lt (mag y) (fexp1 (mag x) - 1)) as [Hly|Hly].
   rewrite (round_generic beta fexp2).
   + reflexivity.
   + now apply valid_rnd_N.
-  + assert (Hf1 : (fexp1 (mag x) <= mag y)%Z); [omega|].
+  + assert (Hf1 : (fexp1 (mag x) <= mag y)%Z) by lia.
     now apply (round_round_plus_radix_ge_3_aux0 fexp1).
 Qed.
 
@@ -1966,7 +1966,7 @@ destruct (Req_dec x 0) as [Zx|Nzx].
   + reflexivity.
   + now apply valid_rnd_N.
   + apply (generic_inclusion_mag beta fexp1).
-    now intros _; apply Hexp4; omega.
+    now intros _; apply Hexp4; lia.
     exact Fy.
 - (* x <> 0 *)
   destruct (Req_dec y 0) as [Zy|Nzy].
@@ -1977,7 +1977,7 @@ destruct (Req_dec x 0) as [Zx|Nzx].
     * reflexivity.
     * now apply valid_rnd_N.
     * apply (generic_inclusion_mag beta fexp1).
-      now intros _; apply Hexp4; omega.
+      now intros _; apply Hexp4; lia.
       exact Fx.
   + (* y <> 0 *)
     assert (Px : 0 < x); [lra|].
@@ -2009,21 +2009,21 @@ assert (Lyx : (mag y <= mag x)%Z);
 destruct (Z.lt_ge_cases (mag x - 2) (mag y)) as [Hlt|Hge].
 - (* mag x - 2 < mag y *)
   assert (Hor : (mag y = mag x :> Z)
-                \/ (mag y = mag x - 1 :> Z)%Z); [omega|].
+                \/ (mag y = mag x - 1 :> Z)%Z) by lia.
   destruct Hor as [Heq|Heqm1].
   + (* mag y = mag x *)
     apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy].
     * apply Hexp4.
-      apply Z.le_trans with (mag (x - y)); [omega|].
+      apply Z.le_trans with (mag (x - y)); [lia|].
       now apply mag_minus.
     * rewrite Heq.
       apply Hexp4.
-      apply Z.le_trans with (mag (x - y)); [omega|].
+      apply Z.le_trans with (mag (x - y)); [lia|].
       now apply mag_minus.
   + (* mag y = mag x - 1 *)
     apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy].
     * apply Hexp4.
-      apply Z.le_trans with (mag (x - y)); [omega|].
+      apply Z.le_trans with (mag (x - y)); [lia|].
       now apply mag_minus.
     * rewrite Heqm1.
       apply Hexp4.
@@ -2034,7 +2034,7 @@ destruct (Z.lt_ge_cases (mag x - 2) (mag y)) as [Hlt|Hge].
   + (* mag (x - y) = mag x *)
     apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy].
     * apply Hexp4.
-      omega.
+      lia.
     * now rewrite Lxmy; apply Hexp3.
   + (* mag (x - y) = mag x - 1 *)
     apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy];
@@ -2071,8 +2071,8 @@ assert (Hfy : (fexp1 (mag y) < mag y)%Z);
   [now apply mag_generic_gt; [|apply Rgt_not_eq|]|].
 apply (round_round_minus_aux0_aux fexp1); [| |exact Fx|exact Fy].
 - apply Z.le_trans with (fexp1 (mag (x - y))).
-  + apply Hexp4; omega.
-  + omega.
+  + apply Hexp4; lia.
+  + lia.
 - now apply Hexp3.
 Qed.
 
@@ -2097,7 +2097,7 @@ intros Hbeta fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Py Hxy Hly Hly'
 assert (Px := Rlt_trans 0 y x Py Hxy).
 destruct Hexp as (_,(_,(_,Hexp4))).
 assert (Hf2 : (fexp2 (mag x) <= fexp1 (mag x))%Z);
-  [now apply Hexp4; omega|].
+  [now apply Hexp4; lia|].
 assert (Hfx : (fexp1 (mag x) < mag x)%Z);
   [now apply mag_generic_gt; [|apply Rgt_not_eq|]|].
 assert (Bpow3 : bpow (- 1) <= / 3).
@@ -2113,12 +2113,12 @@ apply round_round_gt_mid.
 - exact Vfexp1.
 - exact Vfexp2.
 - lra.
-- apply Hexp4; omega.
-- assert (fexp1 (mag (x - y)) < mag (x - y))%Z; [|omega].
+- apply Hexp4; lia.
+- assert (fexp1 (mag (x - y)) < mag (x - y))%Z; [|lia].
   apply (valid_exp_large fexp1 (mag x - 1)).
-  + apply (valid_exp_large fexp1 (mag y)); [|omega].
+  + apply (valid_exp_large fexp1 (mag y)); [|lia].
     now apply mag_generic_gt; [|apply Rgt_not_eq|].
-  + now apply mag_minus_lb; [| |omega].
+  + now apply mag_minus_lb; [| |lia].
 - unfold midp'.
   apply (Rplus_lt_reg_r (/ 2 * ulp beta fexp1 (x - y) - (x - y))).
   ring_simplify.
@@ -2135,7 +2135,7 @@ apply round_round_gt_mid.
     apply Rmult_le_compat_r; [now apply bpow_ge_0|].
     unfold Raux.bpow, Z.pow_pos; simpl.
     rewrite Zmult_1_r; apply Rinv_le; [lra|].
-    now apply IZR_le; omega.
+    now apply IZR_le; lia.
 - intro Hf2'.
   unfold midp'.
   apply (Rplus_lt_reg_r (/ 2 * (ulp beta fexp1 (x - y)
@@ -2164,7 +2164,7 @@ apply round_round_gt_mid.
     replace (_ - _) with (- / 3) by field.
     apply Ropp_le_contravar.
     apply Rle_trans with (bpow (- 1)).
-    * apply bpow_le; omega.
+    * apply bpow_le; lia.
     * unfold Raux.bpow, Z.pow_pos; simpl.
       rewrite Zmult_1_r; apply Rinv_le; [lra|].
       now apply IZR_le.
@@ -2204,12 +2204,12 @@ destruct (Req_dec y x) as [Hy|Hy].
       { rewrite (round_generic beta fexp2).
         - reflexivity.
         - now apply valid_rnd_N.
-        - assert (Hf1 : (fexp1 (mag (x - y)) <= mag y)%Z); [omega|].
+        - assert (Hf1 : (fexp1 (mag (x - y)) <= mag y)%Z) by lia.
           now apply (round_round_minus_radix_ge_3_aux1 fexp1). }
   + rewrite (round_generic beta fexp2).
     * reflexivity.
     * now apply valid_rnd_N.
-    * assert (Hf1 : (fexp1 (mag x) <= mag y)%Z); [omega|].
+    * assert (Hf1 : (fexp1 (mag x) <= mag y)%Z) by lia.
       now apply (round_round_minus_radix_ge_3_aux0 fexp1).
 Qed.
 
@@ -2236,7 +2236,7 @@ destruct (Req_dec x 0) as [Zx|Nzx].
   * now apply valid_rnd_N.
   * apply (generic_inclusion_mag beta fexp1).
     destruct Hexp as (_,(_,(_,Hexp4))).
-    now intros _; apply Hexp4; omega.
+    now intros _; apply Hexp4; lia.
     exact Fy.
 - (* x <> 0 *)
   destruct (Req_dec y 0) as [Zy|Nzy].
@@ -2247,7 +2247,7 @@ destruct (Req_dec x 0) as [Zx|Nzx].
     * now apply valid_rnd_N.
     * apply (generic_inclusion_mag beta fexp1).
       destruct Hexp as (_,(_,(_,Hexp4))).
-      now intros _; apply Hexp4; omega.
+      now intros _; apply Hexp4; lia.
       exact Fx.
   + (* y <> 0 *)
     assert (Px : 0 < x); [lra|].
@@ -2332,9 +2332,9 @@ Proof.
 intros Hprec.
 unfold FLX_exp.
 unfold round_round_plus_radix_ge_3_hyp; split; [|split; [|split]];
-intros ex ey; try omega.
+intros ex ey; try lia.
 unfold Prec_gt_0 in prec_gt_0_.
-omega.
+lia.
 Qed.
 
 Theorem round_round_plus_radix_ge_3_FLX :
@@ -2393,19 +2393,19 @@ unfold round_round_plus_radix_ge_3_hyp; split; [|split; [|split]]; intros ex ey.
 - generalize (Zmax_spec (ex + 1 - prec) emin).
   generalize (Zmax_spec (ex - prec') emin').
   generalize (Zmax_spec (ey - prec) emin).
-  omega.
+  lia.
 - generalize (Zmax_spec (ex - 1 - prec) emin).
   generalize (Zmax_spec (ex - prec') emin').
   generalize (Zmax_spec (ey - prec) emin).
-  omega.
+  lia.
 - generalize (Zmax_spec (ex - prec) emin).
   generalize (Zmax_spec (ex - prec') emin').
   generalize (Zmax_spec (ey - prec) emin).
-  omega.
+  lia.
 - unfold Prec_gt_0 in prec_gt_0_.
   generalize (Zmax_spec (ex - prec') emin').
   generalize (Zmax_spec (ey - prec) emin).
-  omega.
+  lia.
 Qed.
 
 Theorem round_round_plus_radix_ge_3_FLT :
@@ -2467,18 +2467,18 @@ unfold round_round_plus_radix_ge_3_hyp; split; [|split; [|split]]; intros ex ey.
 - destruct (Z.ltb_spec (ex + 1 - prec) emin);
   destruct (Z.ltb_spec (ex - prec') emin');
   destruct (Z.ltb_spec (ey - prec) emin);
-  omega.
+  lia.
 - destruct (Z.ltb_spec (ex - 1 - prec) emin);
   destruct (Z.ltb_spec (ex - prec') emin');
   destruct (Z.ltb_spec (ey - prec) emin);
-  omega.
+  lia.
 - destruct (Z.ltb_spec (ex - prec) emin);
   destruct (Z.ltb_spec (ex - prec') emin');
   destruct (Z.ltb_spec (ey - prec) emin);
-  omega.
+  lia.
 - destruct (Z.ltb_spec (ex - prec') emin');
   destruct (Z.ltb_spec (ey - prec) emin);
-  omega.
+  lia.
 Qed.
 
 Theorem round_round_plus_radix_ge_3_FTZ :
@@ -2546,11 +2546,11 @@ intros Cmid.
 destruct (generic_format_EM beta fexp1 x) as [Fx|Nfx].
 - (* generic_format beta fexp1 x *)
   rewrite (round_generic beta fexp2); [reflexivity|now apply valid_rnd_N|].
-  now apply (generic_inclusion_mag beta fexp1); [omega|].
+  now apply (generic_inclusion_mag beta fexp1); [lia|].
 - (* ~ generic_format beta fexp1 x *)
   assert (Hceil : round beta fexp1 Zceil x = rd + u1);
   [now apply round_UP_DN_ulp|].
-  assert (Hf2' : (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z); [omega|].
+  assert (Hf2' : (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z) by lia.
   destruct (Rlt_or_le (x - rd) (/ 2 * (u1 - u2))).
   + (* x - rd < / 2 * (u1 - u2) *)
     apply round_round_lt_mid_further_place; try assumption.
@@ -2587,7 +2587,7 @@ Proof.
 intros x Px.
 rewrite (mag_sqrt beta x Px).
 generalize (Zdiv2_odd_eqn (mag x + 1)).
-destruct Z.odd ; intros ; omega.
+destruct Z.odd ; intros ; lia.
 Qed.
 
 Lemma round_round_sqrt_aux :
@@ -2638,7 +2638,7 @@ assert (Pb : 0 < b).
   apply Rlt_Rminus.
   unfold u2, u1.
   apply bpow_lt.
-  omega. }
+  lia. }
 assert (Pb' : 0 < b').
 { now unfold b'; rewrite Rmult_plus_distr_l; apply Rplus_lt_0_compat. }
 assert (Hr : sqrt x <= a + b').
@@ -2654,7 +2654,7 @@ assert (Hf1 : (2 * fexp1 (mag (sqrt x)) <= fexp1 (mag (x)))%Z);
   [destruct (mag_sqrt_disj x Px) as [H'|H']; rewrite H'; apply Hexp|].
 assert (Hlx : (fexp1 (2 * mag (sqrt x)) < 2 * mag (sqrt x))%Z).
 { destruct (mag_sqrt_disj x Px) as [Hlx|Hlx].
-  - apply (valid_exp_large fexp1 (mag x)); [|omega].
+  - apply (valid_exp_large fexp1 (mag x)); [|lia].
     now apply mag_generic_gt; [|apply Rgt_not_eq|].
   - rewrite <- Hlx.
     now apply mag_generic_gt; [|apply Rgt_not_eq|]. }
@@ -2698,7 +2698,7 @@ destruct (Req_dec a 0) as [Za|Nza].
     unfold b'; change (bpow _) with u1.
     apply Rlt_le_trans with (/ 2 * (u1 + u1)); [|lra].
     apply Rmult_lt_compat_l; [lra|]; apply Rplus_lt_compat_l.
-    unfold u2, u1, ulp, cexp; apply bpow_lt; omega.
+    unfold u2, u1, ulp, cexp; apply bpow_lt; lia.
 - (* a <> 0 *)
   assert (Pa : 0 < a); [lra|].
   assert (Hla : (mag a = mag (sqrt x) :> Z)).
@@ -2731,7 +2731,7 @@ destruct (Req_dec a 0) as [Za|Nza].
         * apply pow2_ge_0.
         * unfold Raux.bpow, Z.pow_pos; simpl; rewrite Zmult_1_r.
           apply Rinv_le; [lra|].
-          change 4%Z with (2 * 2)%Z; apply IZR_le, Zmult_le_compat; omega.
+          change 4%Z with (2 * 2)%Z; apply IZR_le, Zmult_le_compat; lia.
         * rewrite <- (Rplus_0_l (u1 ^ 2)) at 1; apply Rplus_le_compat_r.
           apply pow2_ge_0. }
   assert (Hr' : x <= a * a + u1 * a).
@@ -2744,11 +2744,11 @@ destruct (Req_dec a 0) as [Za|Nza].
     apply (Rmult_le_reg_r (bpow (- 2 * fexp1 (mag (sqrt x)))));
       [now apply bpow_gt_0|bpow_simplify].
     rewrite Fx at 1; bpow_simplify.
-    rewrite <- IZR_Zpower; [|omega].
+    rewrite <- IZR_Zpower; [|lia].
     rewrite <- plus_IZR, <- 2!mult_IZR.
     apply IZR_le, Zlt_succ_le, lt_IZR.
     unfold Z.succ; rewrite plus_IZR; do 2 rewrite mult_IZR; rewrite plus_IZR.
-    rewrite IZR_Zpower; [|omega].
+    rewrite IZR_Zpower; [|lia].
     apply (Rmult_lt_reg_r (bpow (2 * fexp1 (mag (sqrt x)))));
       [now apply bpow_gt_0|bpow_simplify].
     rewrite <- Fx.
@@ -2787,12 +2787,12 @@ destruct (Req_dec a 0) as [Za|Nza].
           apply Rinv_le; [lra|].
           apply IZR_le.
           rewrite <- (Zmult_1_l 2).
-          apply Zmult_le_compat; omega.
+          apply Zmult_le_compat; lia.
       + assert (u2 ^ 2 < u1 ^ 2); [|unfold b'; lra].
         unfold pow; do 2 rewrite Rmult_1_r.
         assert (H' : 0 <= u2); [unfold u2, ulp; apply bpow_ge_0|].
         assert (u2 < u1); [|now apply Rmult_lt_compat].
-        unfold u1, u2, ulp, cexp; apply bpow_lt; omega. }
+        unfold u1, u2, ulp, cexp; apply bpow_lt; lia. }
   apply (Rlt_irrefl (a * a + u1 * a)).
   apply Rlt_le_trans with (a * a + u1 * a - u2 * a + b * b).
   + rewrite <- (Rplus_0_r (a * a + _)) at 1.
@@ -2835,7 +2835,8 @@ destruct (Rle_or_lt x 0) as [Npx|Px].
       generalize ((proj1 (proj2 Hexp)) 1%Z).
       replace (_ - 1)%Z with 1%Z by ring.
       intro Hexp10.
-      assert (Hf0 : (fexp1 1 < 1)%Z); [omega|clear Hexp10].
+      assert (Hf0 : (fexp1 1 < 1)%Z) by lia.
+      clear Hexp10.
       apply (valid_exp_large fexp1 1); [exact Hf0|].
       apply mag_ge_bpow.
       rewrite Zeq_minus; [|reflexivity].
@@ -2847,18 +2848,18 @@ destruct (Rle_or_lt x 0) as [Npx|Px].
   assert (Hf2 : (fexp2 (mag (sqrt x)) <= fexp1 (mag (sqrt x)) - 1)%Z).
   { assert (H : (fexp1 (2 * mag (sqrt x)) < 2 * mag (sqrt x))%Z).
     { destruct (mag_sqrt_disj x Px) as [Hlx|Hlx].
-      - apply (valid_exp_large fexp1 (mag x)); [|omega].
+      - apply (valid_exp_large fexp1 (mag x)); [|lia].
         now apply mag_generic_gt; [|apply Rgt_not_eq|].
       - rewrite <- Hlx.
         now apply mag_generic_gt; [|apply Rgt_not_eq|]. }
     generalize ((proj2 (proj2 Hexp)) (mag (sqrt x)) H).
-    omega. }
+    lia. }
   apply round_round_mid_cases.
   + exact Vfexp1.
   + exact Vfexp2.
   + now apply sqrt_lt_R0.
-  + omega.
-  + omega.
+  + lia.
+  + lia.
   + intros Hmid; casetype False; apply (Rle_not_lt _ _ Hmid).
     apply (round_round_sqrt_aux fexp1 fexp2 Vfexp1 Vfexp2 Hexp x Px Hf2 Fx).
 Qed.
@@ -2878,7 +2879,7 @@ Proof.
 intros Hprec.
 unfold FLX_exp.
 unfold Prec_gt_0 in prec_gt_0_.
-unfold round_round_sqrt_hyp; split; [|split]; intro ex; omega.
+unfold round_round_sqrt_hyp; split; [|split]; intro ex; lia.
 Qed.
 
 Theorem round_round_sqrt_FLX :
@@ -2919,14 +2920,14 @@ unfold Prec_gt_0 in prec_gt_0_.
 unfold round_round_sqrt_hyp; split; [|split]; intros ex.
 - generalize (Zmax_spec (ex - prec) emin).
   generalize (Zmax_spec (2 * ex - prec) emin).
-  omega.
+  lia.
 - generalize (Zmax_spec (ex - prec) emin).
   generalize (Zmax_spec (2 * ex - 1 - prec) emin).
-  omega.
+  lia.
 - generalize (Zmax_spec (2 * ex - prec) emin).
   generalize (Zmax_spec (ex - prec') emin').
   generalize (Zmax_spec (ex - prec) emin).
-  omega.
+  lia.
 Qed.
 
 Theorem round_round_sqrt_FLT :
@@ -2969,18 +2970,18 @@ unfold Prec_gt_0 in *.
 unfold round_round_sqrt_hyp; split; [|split]; intros ex.
 - destruct (Z.ltb_spec (ex - prec) emin);
   destruct (Z.ltb_spec (2 * ex - prec) emin);
-  omega.
+  lia.
 - destruct (Z.ltb_spec (ex - prec) emin);
   destruct (Z.ltb_spec (2 * ex - 1 - prec) emin);
-  omega.
+  lia.
 - intro H.
   destruct (Zle_or_lt emin (2 * ex - prec)) as [H'|H'].
   + destruct (Z.ltb_spec (ex - prec') emin');
     destruct (Z.ltb_spec (ex - prec) emin);
-    omega.
+    lia.
   + casetype False.
     rewrite (Zlt_bool_true _ _ H') in H.
-    omega.
+    lia.
 Qed.
 
 Theorem round_round_sqrt_FTZ :
@@ -3057,7 +3058,7 @@ assert (Pb : 0 < b).
   apply Rlt_Rminus.
   unfold u2, u1, ulp, cexp.
   apply bpow_lt.
-  omega. }
+  lia. }
 assert (Pb' : 0 < b').
 { now unfold b'; rewrite Rmult_plus_distr_l; apply Rplus_lt_0_compat. }
 assert (Hr : sqrt x <= a + b').
@@ -3073,7 +3074,7 @@ assert (Hf1 : (2 * fexp1 (mag (sqrt x)) <= fexp1 (mag (x)))%Z);
   [destruct (mag_sqrt_disj x Px) as [H'|H']; rewrite H'; apply Hexp|].
 assert (Hlx : (fexp1 (2 * mag (sqrt x)) < 2 * mag (sqrt x))%Z).
 { destruct (mag_sqrt_disj x Px) as [Hlx|Hlx].
-  - apply (valid_exp_large fexp1 (mag x)); [|omega].
+  - apply (valid_exp_large fexp1 (mag x)); [|lia].
     now apply mag_generic_gt; [|apply Rgt_not_eq|].
   - rewrite <- Hlx.
     now apply mag_generic_gt; [|apply Rgt_not_eq|]. }
@@ -3117,7 +3118,7 @@ destruct (Req_dec a 0) as [Za|Nza].
     unfold b'; change (bpow _) with u1.
     apply Rlt_le_trans with (/ 2 * (u1 + u1)); [|lra].
     apply Rmult_lt_compat_l; [lra|]; apply Rplus_lt_compat_l.
-    unfold u2, u1, ulp, cexp; apply bpow_lt; omega.
+    unfold u2, u1, ulp, cexp; apply bpow_lt; lia.
 - (* a <> 0 *)
   assert (Pa : 0 < a); [lra|].
   assert (Hla : (mag a = mag (sqrt x) :> Z)).
@@ -3162,11 +3163,11 @@ destruct (Req_dec a 0) as [Za|Nza].
     apply (Rmult_le_reg_r (bpow (- 2 * fexp1 (mag (sqrt x)))));
       [now apply bpow_gt_0|bpow_simplify].
     rewrite Fx at 1; bpow_simplify.
-    rewrite <- IZR_Zpower; [|omega].
+    rewrite <- IZR_Zpower; [|lia].
     rewrite <- plus_IZR, <- 2!mult_IZR.
     apply IZR_le, Zlt_succ_le, lt_IZR.
     unfold Z.succ; rewrite plus_IZR; do 2 rewrite mult_IZR; rewrite plus_IZR.
-    rewrite IZR_Zpower; [|omega].
+    rewrite IZR_Zpower; [|lia].
     apply (Rmult_lt_reg_r (bpow (2 * fexp1 (mag (sqrt x)))));
       [now apply bpow_gt_0|bpow_simplify].
     rewrite <- Fx.
@@ -3203,12 +3204,12 @@ destruct (Req_dec a 0) as [Za|Nza].
           unfold Raux.bpow; simpl; unfold Z.pow_pos; simpl.
           rewrite Zmult_1_r.
           apply Rinv_le; [lra|].
-          apply IZR_le; omega.
+          apply IZR_le; lia.
       + assert (u2 ^ 2 < u1 ^ 2); [|unfold b'; lra].
         unfold pow; do 2 rewrite Rmult_1_r.
         assert (H' : 0 <= u2); [unfold u2, ulp; apply bpow_ge_0|].
         assert (u2 < u1); [|now apply Rmult_lt_compat].
-        unfold u1, u2, ulp, cexp; apply bpow_lt; omega. }
+        unfold u1, u2, ulp, cexp; apply bpow_lt; lia. }
   apply (Rlt_irrefl (a * a + u1 * a)).
   apply Rlt_le_trans with (a * a + u1 * a - u2 * a + b * b).
   + rewrite <- (Rplus_0_r (a * a + _)) at 1.
@@ -3263,7 +3264,8 @@ destruct (Rle_or_lt x 0) as [Npx|Px].
       generalize ((proj1 (proj2 Hexp)) 1%Z).
       replace (_ - 1)%Z with 1%Z by ring.
       intro Hexp10.
-      assert (Hf0 : (fexp1 1 < 1)%Z); [omega|clear Hexp10].
+      assert (Hf0 : (fexp1 1 < 1)%Z) by lia.
+      clear Hexp10.
       apply (valid_exp_large fexp1 1); [exact Hf0|].
       apply mag_ge_bpow.
       rewrite Zeq_minus; [|reflexivity].
@@ -3275,18 +3277,18 @@ destruct (Rle_or_lt x 0) as [Npx|Px].
   assert (Hf2 : (fexp2 (mag (sqrt x)) <= fexp1 (mag (sqrt x)) - 1)%Z).
   { assert (H : (fexp1 (2 * mag (sqrt x)) < 2 * mag (sqrt x))%Z).
     { destruct (mag_sqrt_disj x Px) as [Hlx|Hlx].
-      - apply (valid_exp_large fexp1 (mag x)); [|omega].
+      - apply (valid_exp_large fexp1 (mag x)); [|lia].
         now apply mag_generic_gt; [|apply Rgt_not_eq|].
       - rewrite <- Hlx.
         now apply mag_generic_gt; [|apply Rgt_not_eq|]. }
     generalize ((proj2 (proj2 Hexp)) (mag (sqrt x)) H).
-    omega. }
+    lia. }
   apply round_round_mid_cases.
   + exact Vfexp1.
   + exact Vfexp2.
   + now apply sqrt_lt_R0.
-  + omega.
-  + omega.
+  + lia.
+  + lia.
   + intros Hmid; casetype False; apply (Rle_not_lt _ _ Hmid).
     apply (round_round_sqrt_radix_ge_4_aux Hbeta fexp1 fexp2 Vfexp1 Vfexp2
                                            Hexp x Px Hf2 Fx).
@@ -3307,7 +3309,7 @@ Proof.
 intros Hprec.
 unfold FLX_exp.
 unfold Prec_gt_0 in prec_gt_0_.
-unfold round_round_sqrt_radix_ge_4_hyp; split; [|split]; intro ex; omega.
+unfold round_round_sqrt_radix_ge_4_hyp; split; [|split]; intro ex; lia.
 Qed.
 
 Theorem round_round_sqrt_radix_ge_4_FLX :
@@ -3350,14 +3352,14 @@ unfold Prec_gt_0 in prec_gt_0_.
 unfold round_round_sqrt_radix_ge_4_hyp; split; [|split]; intros ex.
 - generalize (Zmax_spec (ex - prec) emin).
   generalize (Zmax_spec (2 * ex - prec) emin).
-  omega.
+  lia.
 - generalize (Zmax_spec (ex - prec) emin).
   generalize (Zmax_spec (2 * ex - 1 - prec) emin).
-  omega.
+  lia.
 - generalize (Zmax_spec (2 * ex - prec) emin).
   generalize (Zmax_spec (ex - prec') emin').
   generalize (Zmax_spec (ex - prec) emin).
-  omega.
+  lia.
 Qed.
 
 Theorem round_round_sqrt_radix_ge_4_FLT :
@@ -3402,18 +3404,18 @@ unfold Prec_gt_0 in *.
 unfold round_round_sqrt_radix_ge_4_hyp; split; [|split]; intros ex.
 - destruct (Z.ltb_spec (ex - prec) emin);
   destruct (Z.ltb_spec (2 * ex - prec) emin);
-  omega.
+  lia.
 - destruct (Z.ltb_spec (ex - prec) emin);
   destruct (Z.ltb_spec (2 * ex - 1 - prec) emin);
-  omega.
+  lia.
 - intro H.
   destruct (Zle_or_lt emin (2 * ex - prec)) as [H'|H'].
   + destruct (Z.ltb_spec (ex - prec') emin');
     destruct (Z.ltb_spec (ex - prec) emin);
-    omega.
+    lia.
   + casetype False.
     rewrite (Zlt_bool_true _ _ H') in H.
-    omega.
+    lia.
 Qed.
 
 Theorem round_round_sqrt_radix_ge_4_FTZ :
@@ -3479,7 +3481,7 @@ assert (Hf : F2R f = x).
   rewrite plus_IZR.
   rewrite Rmult_plus_distr_r.
   rewrite mult_IZR.
-  rewrite IZR_Zpower; [|omega].
+  rewrite IZR_Zpower; [|lia].
   unfold cexp at 2; bpow_simplify.
   unfold Zminus; rewrite bpow_plus.
   rewrite (Rmult_comm _ (bpow (- 1))).
@@ -3489,11 +3491,11 @@ assert (Hf : F2R f = x).
   rewrite Ebeta.
   rewrite (mult_IZR 2).
   rewrite Rinv_mult_distr;
-    [|simpl; lra | apply IZR_neq; omega].
+    [|simpl; lra | apply IZR_neq; lia].
   rewrite <- Rmult_assoc; rewrite (Rmult_comm (IZR n));
   rewrite (Rmult_assoc _ (IZR n)).
   rewrite Rinv_r;
-    [rewrite Rmult_1_r | apply IZR_neq; omega].
+    [rewrite Rmult_1_r | apply IZR_neq; lia].
   simpl; fold (cexp beta fexp1 x).
   rewrite <- 2!ulp_neq_0; try now apply Rgt_not_eq.
   fold u; rewrite Xmid at 2.
@@ -3525,12 +3527,12 @@ assert (Hf : F2R f = x).
     unfold round, F2R, scaled_mantissa, cexp; simpl.
     bpow_simplify.
     rewrite Lrd.
-    rewrite <- (IZR_Zpower _ (_ - _)); [|omega].
+    rewrite <- (IZR_Zpower _ (_ - _)); [|lia].
     rewrite <- mult_IZR.
     rewrite (Zfloor_imp (Zfloor (x * bpow (- fexp1 (mag x))) *
                          beta ^ (fexp1 (mag x) - fexp2 (mag x)))).
     + rewrite mult_IZR.
-      rewrite IZR_Zpower; [|omega].
+      rewrite IZR_Zpower; [|lia].
       bpow_simplify.
       now unfold rd.
     + split; [now apply Rle_refl|].
@@ -3557,7 +3559,7 @@ assert (Hlx : bpow (mag x - 1) <= x < bpow (mag x)).
   apply Hex.
   now apply Rgt_not_eq. }
 unfold round_round_eq.
-rewrite (round_N_small_pos beta fexp1 _ x (mag x)); [|exact Hlx|omega].
+rewrite (round_N_small_pos beta fexp1 _ x (mag x)); [|exact Hlx|lia].
 set (x'' := round beta fexp2 (Znearest choice2) x).
 destruct (Req_dec x'' 0) as [Zx''|Nzx''];
   [now rewrite Zx''; rewrite round_0; [|apply valid_rnd_N]|].
@@ -3566,7 +3568,7 @@ destruct (Zle_or_lt (fexp2 (mag x)) (mag x)).
   destruct (Rlt_or_le x'' (bpow (mag x))).
   + (* x'' < bpow (mag x) *)
     rewrite (round_N_small_pos beta fexp1 _ _ (mag x));
-    [reflexivity|split; [|exact H0]|omega].
+    [reflexivity|split; [|exact H0]|lia].
     apply round_large_pos_ge_bpow; [now apply valid_rnd_N| |now apply Hlx].
     fold x''; assert (0 <= x''); [|lra]; unfold x''.
     rewrite <- (round_0 beta fexp2 (Znearest choice2)).
@@ -3581,7 +3583,7 @@ destruct (Zle_or_lt (fexp2 (mag x)) (mag x)).
     unfold round, F2R, scaled_mantissa, cexp; simpl.
     rewrite mag_bpow.
     assert (Hf11 : (fexp1 (mag x + 1) = fexp1 (mag x) :> Z)%Z);
-      [apply Vfexp1; omega|].
+      [apply Vfexp1; lia|].
     rewrite Hf11.
     apply (Rmult_eq_reg_r (bpow (- fexp1 (mag x))));
       [|now apply Rgt_not_eq; apply bpow_gt_0].
@@ -3590,7 +3592,7 @@ destruct (Zle_or_lt (fexp2 (mag x)) (mag x)).
     apply Znearest_imp.
     simpl; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r.
     rewrite Rabs_right; [|now apply Rle_ge; apply bpow_ge_0].
-    apply Rle_lt_trans with (bpow (- 2)); [now apply bpow_le; omega|].
+    apply Rle_lt_trans with (bpow (- 2)); [now apply bpow_le; lia|].
     unfold Raux.bpow, Z.pow_pos; simpl; rewrite Zmult_1_r.
     assert (Hbeta : (2 <= beta)%Z).
     { destruct beta as (beta_val,beta_prop); simpl.
@@ -3598,11 +3600,11 @@ destruct (Zle_or_lt (fexp2 (mag x)) (mag x)).
     apply Rinv_lt_contravar.
     * apply Rmult_lt_0_compat; [lra|].
       rewrite mult_IZR; apply Rmult_lt_0_compat;
-      apply IZR_lt; omega.
+      apply IZR_lt; lia.
     * apply IZR_lt.
       apply (Z.le_lt_trans _ _ _ Hbeta).
       rewrite <- (Zmult_1_r beta) at 1.
-      apply Zmult_lt_compat_l; omega.
+      apply Zmult_lt_compat_l; lia.
 - (* mag x < fexp2 (mag x) *)
   casetype False; apply Nzx''.
   now apply (round_N_small_pos beta _ _ _ (mag x)).
@@ -3630,11 +3632,11 @@ assert (Hlx : bpow (mag x - 1) <= x < bpow (mag x)).
   apply Hex.
   now apply Rgt_not_eq. }
 rewrite (round_N_small_pos beta fexp1 choice1 x (mag x));
-  [|exact Hlx|omega].
+  [|exact Hlx|lia].
 destruct (Req_dec x'' 0) as [Zx''|Nzx''];
   [now rewrite Zx''; rewrite round_0; [reflexivity|apply valid_rnd_N]|].
 rewrite (round_N_small_pos beta _ _ x'' (mag x));
-  [reflexivity| |omega].
+  [reflexivity| |lia].
 split.
 - apply round_large_pos_ge_bpow.
   + now apply valid_rnd_N.
@@ -3680,19 +3682,19 @@ set (u2 := ulp beta fexp2 x).
 intros Cz Clt Ceq Cgt.
 destruct (Ztrichotomy (mag x) (fexp1 (mag x) - 1)) as [Hlt|[Heq|Hgt]].
 - (* mag x < fexp1 (mag x) - 1 *)
-  assert (H : (mag x <= fexp1 (mag x) - 2)%Z) by omega.
+  assert (H : (mag x <= fexp1 (mag x) - 2)%Z) by lia.
   now apply round_round_really_zero.
 - (* mag x = fexp1 (mag x) - 1 *)
-  assert (H : (fexp1 (mag x) = (mag x + 1))%Z) by omega.
+  assert (H : (fexp1 (mag x) = (mag x + 1))%Z) by lia.
   destruct (Rlt_or_le x (bpow (mag x) - / 2 * u2)) as [Hlt'|Hge'].
   + now apply round_round_zero.
   + now apply Cz.
 - (* mag x > fexp1 (mag x) - 1 *)
-  assert (H : (fexp1 (mag x) <= mag x)%Z) by omega.
+  assert (H : (fexp1 (mag x) <= mag x)%Z) by lia.
   destruct (Rtotal_order x (midp fexp1 x)) as [Hlt'|[Heq'|Hgt']].
   + (* x < midp fexp1 x *)
     destruct (Rlt_or_le x (midp fexp1 x - / 2 * u2)) as [Hlt''|Hle''].
-    * now apply round_round_lt_mid_further_place; [| | |omega| |].
+    * now apply round_round_lt_mid_further_place; [| | |lia| |].
     * now apply Clt; [|split].
   + (* x = midp fexp1 x *)
     now apply Ceq.
@@ -3703,12 +3705,11 @@ destruct (Ztrichotomy (mag x) (fexp1 (mag x) - 1)) as [Hlt|[Heq|Hgt]].
         - (* generic_format beta fexp1 x *)
           unfold round_round_eq; rewrite (round_generic beta fexp2);
           [reflexivity|now apply valid_rnd_N|].
-          now apply (generic_inclusion_mag beta fexp1); [omega|].
+          now apply (generic_inclusion_mag beta fexp1); [lia|].
         - (* ~ generic_format beta fexp1 x *)
           assert (Hceil : round beta fexp1 Zceil x = x' + u1);
           [now apply round_UP_DN_ulp|].
-          assert (Hf2' : (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z);
-            [omega|].
+          assert (Hf2' : (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z) by lia.
           assert (midp' fexp1 x + / 2 * ulp beta fexp2 x < x);
             [|now apply round_round_gt_mid_further_place].
           revert Hle''; unfold midp, midp'; fold x'.
@@ -3724,7 +3725,7 @@ Lemma mag_div_disj :
 Proof.
 intros x y Px Py.
 generalize (mag_div beta x y (Rgt_not_eq _ _ Px) (Rgt_not_eq _ _ Py)).
-omega.
+lia.
 Qed.
 
 Definition round_round_div_hyp fexp1 fexp2 :=
@@ -3829,7 +3830,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - mag (x / y)
       replace (_ - _ + 1)%Z with ((mag x + 1) - mag y)%Z by ring.
       apply Hexp.
       { now assert (fexp1 (mag x + 1) <= mag x)%Z;
-        [apply valid_exp|omega]. }
+        [apply valid_exp|lia]. }
       { assumption. }
       replace (_ + 1 - _)%Z with (mag x - mag y + 1)%Z by ring.
       now rewrite <- Hxy.
@@ -3842,7 +3843,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - mag (x / y)
     bpow_simplify.
     rewrite (Rmult_comm p).
     unfold p; bpow_simplify.
-    rewrite <- IZR_Zpower; [|omega].
+    rewrite <- IZR_Zpower; [|lia].
     rewrite <- mult_IZR.
     rewrite <- minus_IZR.
     apply IZR_le.
@@ -3850,7 +3851,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - mag (x / y)
     apply Zlt_le_succ.
     apply lt_IZR.
     rewrite mult_IZR.
-    rewrite IZR_Zpower; [|omega].
+    rewrite IZR_Zpower; [|lia].
     apply (Rmult_lt_reg_r (bpow (fexp1 (mag x))));
       [now apply bpow_gt_0|bpow_simplify].
     rewrite <- Fx.
@@ -4000,7 +4001,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y))
       replace (_ - _ + 1)%Z with ((mag x + 1) - mag y)%Z by ring.
       apply Hexp.
       { now assert (fexp1 (mag x + 1) <= mag x)%Z;
-        [apply valid_exp|omega]. }
+        [apply valid_exp|lia]. }
       { assumption. }
       replace (_ + 1 - _)%Z with (mag x - mag y + 1)%Z by ring.
       now rewrite <- Hxy.
@@ -4016,7 +4017,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y))
     rewrite (Rmult_comm u1).
     unfold x', u1, round, F2R, ulp, scaled_mantissa, cexp; simpl.
     bpow_simplify.
-    rewrite <- (IZR_Zpower _ (_ - _)%Z); [|omega].
+    rewrite <- (IZR_Zpower _ (_ - _)%Z); [|lia].
     do 5 rewrite <- mult_IZR.
     rewrite <- plus_IZR.
     rewrite <- minus_IZR.
@@ -4026,7 +4027,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y))
     apply lt_IZR.
     rewrite plus_IZR.
     do 5 rewrite mult_IZR; simpl.
-    rewrite IZR_Zpower; [|omega].
+    rewrite IZR_Zpower; [|lia].
     apply (Rmult_lt_reg_r (bpow (fexp1 (mag x))));
       [now apply bpow_gt_0|].
     rewrite Rmult_assoc.
@@ -4063,7 +4064,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y))
       apply (Zplus_le_reg_r _ _ (- mag y)); ring_simplify.
       rewrite (Zplus_comm (- _)).
       destruct (mag_div_disj x y Px Py) as [Hxy|Hxy]; rewrite Hxy;
-      apply Hexp; try assumption; rewrite <- Hxy; omega.
+      apply Hexp; try assumption; rewrite <- Hxy; lia.
 Qed.
 
 Lemma round_round_div_aux2 :
@@ -4139,7 +4140,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y))
       replace (_ - _ + 1)%Z with ((mag x + 1) - mag y)%Z by ring.
       apply Hexp.
       { now assert (fexp1 (mag x + 1) <= mag x)%Z;
-        [apply valid_exp|omega]. }
+        [apply valid_exp|lia]. }
       { assumption. }
       replace (_ + 1 - _)%Z with (mag x - mag y + 1)%Z by ring.
       now rewrite <- Hxy.
@@ -4213,7 +4214,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y))
       apply (Zplus_le_reg_r _ _ (- mag y)); ring_simplify.
       rewrite (Zplus_comm (- _)).
       destruct (mag_div_disj x y Px Py) as [Hxy|Hxy]; rewrite Hxy;
-      apply Hexp; try assumption; rewrite <- Hxy; omega.
+      apply Hexp; try assumption; rewrite <- Hxy; lia.
   + apply Rge_le; rewrite Fx at 1; apply Rle_ge.
     rewrite Fy at 1 2.
     apply (Rmult_le_reg_r (bpow (- fexp1 (mag x))));
@@ -4225,7 +4226,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y))
     rewrite (Rmult_comm u1).
     unfold x', u1, round, F2R, ulp, scaled_mantissa, cexp; simpl.
     bpow_simplify.
-    rewrite <- (IZR_Zpower _ (_ - _)%Z); [|omega].
+    rewrite <- (IZR_Zpower _ (_ - _)%Z); [|lia].
     do 5 rewrite <- mult_IZR.
     do 2 rewrite <- plus_IZR.
     apply IZR_le.
@@ -4233,7 +4234,7 @@ destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y))
     apply lt_IZR.
     rewrite plus_IZR.
     do 5 rewrite mult_IZR; simpl.
-    rewrite IZR_Zpower; [|omega].
+    rewrite IZR_Zpower; [|lia].
     apply (Rmult_lt_reg_r (bpow (fexp1 (mag x))));
       [now apply bpow_gt_0|].
     rewrite (Rmult_assoc _ (IZR mx)).
@@ -4379,8 +4380,8 @@ intros Hprec.
 unfold Prec_gt_0 in prec_gt_0_.
 unfold FLX_exp.
 unfold round_round_div_hyp.
-split; [now intro ex; omega|].
-split; [|split; [|split]]; intros ex ey; omega.
+split; [now intro ex; lia|].
+split; [|split; [|split]]; intros ex ey; lia.
 Qed.
 
 Theorem round_round_div_FLX :
@@ -4425,27 +4426,27 @@ unfold round_round_div_hyp.
 split; [intro ex|split; [|split; [|split]]; intros ex ey].
 - generalize (Zmax_spec (ex - prec') emin').
   generalize (Zmax_spec (ex - prec) emin).
-  omega.
+  lia.
 - generalize (Zmax_spec (ex - prec) emin).
   generalize (Zmax_spec (ey - prec) emin).
   generalize (Zmax_spec (ex - ey - prec) emin).
   generalize (Zmax_spec (ex - ey - prec') emin').
-  omega.
+  lia.
 - generalize (Zmax_spec (ex - prec) emin).
   generalize (Zmax_spec (ey - prec) emin).
   generalize (Zmax_spec (ex - ey + 1 - prec) emin).
   generalize (Zmax_spec (ex - ey + 1 - prec') emin').
-  omega.
+  lia.
 - generalize (Zmax_spec (ex - prec) emin).
   generalize (Zmax_spec (ey - prec) emin).
   generalize (Zmax_spec (ex - ey - prec) emin).
   generalize (Zmax_spec (ex - ey - prec') emin').
-  omega.
+  lia.
 - generalize (Zmax_spec (ex - prec) emin).
   generalize (Zmax_spec (ey - prec) emin).
   generalize (Zmax_spec (ex - ey - prec) emin).
   generalize (Zmax_spec (ex - ey - prec') emin').
-  omega.
+  lia.
 Qed.
 
 Theorem round_round_div_FLT :
@@ -4493,27 +4494,27 @@ unfold round_round_div_hyp.
 split; [intro ex|split; [|split; [|split]]; intros ex ey].
 - destruct (Z.ltb_spec (ex - prec') emin');
   destruct (Z.ltb_spec (ex - prec) emin);
-  omega.
+  lia.
 - destruct (Z.ltb_spec (ex - prec) emin);
   destruct (Z.ltb_spec (ey - prec) emin);
   destruct (Z.ltb_spec (ex - ey - prec) emin);
   destruct (Z.ltb_spec (ex - ey - prec') emin');
-  omega.
+  lia.
 - destruct (Z.ltb_spec (ex - prec) emin);
   destruct (Z.ltb_spec (ey - prec) emin);
   destruct (Z.ltb_spec (ex - ey + 1 - prec) emin);
   destruct (Z.ltb_spec (ex - ey + 1 - prec') emin');
-  omega.
+  lia.
 - destruct (Z.ltb_spec (ex - prec) emin);
   destruct (Z.ltb_spec (ey - prec) emin);
   destruct (Z.ltb_spec (ex - ey - prec) emin);
   destruct (Z.ltb_spec (ex - ey - prec') emin');
-  omega.
+  lia.
 - destruct (Z.ltb_spec (ex - prec) emin);
   destruct (Z.ltb_spec (ey - prec) emin);
   destruct (Z.ltb_spec (ex - ey - prec) emin);
   destruct (Z.ltb_spec (ex - ey - prec') emin');
-  omega.
+  lia.
 Qed.
 
 Theorem round_round_div_FTZ :
diff --git a/flocq/Prop/Mult_error.v b/flocq/Prop/Mult_error.v
index 57a3856f..f4467025 100644
--- a/flocq/Prop/Mult_error.v
+++ b/flocq/Prop/Mult_error.v
@@ -18,6 +18,8 @@ COPYING file for more details.
 *)
 
 (** * Error of the multiplication is in the FLX/FLT format *)
+
+From Coq Require Import Lia.
 Require Import Core Operations Plus_error.
 
 Section Fprop_mult_error.
@@ -71,7 +73,7 @@ unfold cexp, FLX_exp.
 rewrite mag_unique with (1 := Hex).
 rewrite mag_unique with (1 := Hey).
 rewrite mag_unique with (1 := Hexy).
-cut (exy - 1 < ex + ey)%Z. omega.
+cut (exy - 1 < ex + ey)%Z. lia.
 apply (lt_bpow beta).
 apply Rle_lt_trans with (1 := proj1 Hexy).
 rewrite Rabs_mult.
@@ -89,7 +91,7 @@ rewrite mag_unique with (1 := Hey).
 rewrite mag_unique with (1 := Hexy).
 cut ((ex - 1) + (ey - 1) < exy)%Z.
 generalize (prec_gt_0 prec).
-clear ; omega.
+clear ; lia.
 apply (lt_bpow beta).
 apply Rle_lt_trans with (2 := proj2 Hexy).
 rewrite Rabs_mult.
@@ -163,7 +165,7 @@ apply (generic_format_F2R' _ _ _ f).
 { now unfold F2R; simpl; rewrite bpow_plus, Rmult_assoc. }
 intro Nzmx; unfold mx, ex; rewrite <- Fx.
 unfold f, ex; simpl; unfold cexp; rewrite (mag_mult_bpow _ _ _ Nzx).
-unfold FLX_exp; omega.
+unfold FLX_exp; lia.
 Qed.
 
 End Fprop_mult_error.
@@ -209,10 +211,10 @@ assumption.
 apply Rle_trans with (2:=Hxy).
 apply bpow_le.
 generalize (prec_gt_0 prec).
-clear ; omega.
+clear ; lia.
 rewrite <- (round_FLT_FLX beta emin) in H1.
 2:apply Rle_trans with (2:=Hxy).
-2:apply bpow_le ; generalize (prec_gt_0 prec) ; clear ; omega.
+2:apply bpow_le ; generalize (prec_gt_0 prec) ; clear ; lia.
 unfold f; rewrite <- H1.
 apply generic_format_F2R.
 intros _.
@@ -242,7 +244,7 @@ specialize (Ex Hx0).
 destruct (mag beta y) as (ey,Ey) ; simpl.
 specialize (Ey Hy0).
 assert (emin + 2 * prec -1 < ex + ey)%Z.
-2: omega.
+2: lia.
 apply (lt_bpow beta).
 apply Rle_lt_trans with (1:=Hxy).
 rewrite Rabs_mult, bpow_plus.
@@ -262,7 +264,7 @@ intros Hy _.
 rewrite <- (Rmult_1_l (bpow _)) at 1.
 apply Rmult_le_compat_r.
 apply bpow_ge_0.
-apply IZR_le; omega.
+apply IZR_le; lia.
 intros H1 H2; contradict H2.
 replace ny with 0%Z.
 simpl; ring.
@@ -296,7 +298,7 @@ destruct (mag beta x) as (ex,Hx).
 destruct (mag beta y) as (ey,Hy).
 simpl; apply Z.le_trans with ((ex-prec)+(ey-prec))%Z.
 2: apply Zplus_le_compat; apply Z.le_max_l.
-assert (e + 2*prec -1< ex+ey)%Z;[idtac|omega].
+assert (e + 2*prec -1< ex+ey)%Z;[idtac|lia].
 apply lt_bpow with beta.
 apply Rle_lt_trans with (1:=H1).
 rewrite Rabs_mult, bpow_plus.
@@ -327,9 +329,30 @@ apply (generic_format_F2R' _ _ _ f).
 { now unfold F2R; simpl; rewrite bpow_plus, Rmult_assoc. }
 intro Nzmx; unfold mx, ex; rewrite <- Fx.
 unfold f, ex; simpl; unfold cexp; rewrite (mag_mult_bpow _ _ _ Nzx).
-unfold FLT_exp; rewrite Z.max_l; [|omega]; rewrite <- Z.add_max_distr_r.
-set (n := (_ - _ + _)%Z); apply (Z.le_trans _ n); [unfold n; omega|].
+unfold FLT_exp; rewrite Z.max_l; [|lia]; rewrite <- Z.add_max_distr_r.
+set (n := (_ - _ + _)%Z); apply (Z.le_trans _ n); [unfold n; lia|].
 apply Z.le_max_l.
 Qed.
 
+Lemma mult_bpow_pos_exact_FLT :
+  forall x e,
+  format x ->
+  (0 <= e)%Z ->
+  format (x * bpow e)%R.
+Proof.
+intros x e Fx He.
+destruct (Req_dec x 0) as [Zx|Nzx].
+{ rewrite Zx, Rmult_0_l; apply generic_format_0. }
+rewrite Fx.
+set (mx := Ztrunc _); set (ex := cexp _).
+pose (f := {| Fnum := mx; Fexp := ex + e |} : float beta).
+apply (generic_format_F2R' _ _ _ f).
+{ now unfold F2R; simpl; rewrite bpow_plus, Rmult_assoc. }
+intro Nzmx; unfold mx, ex; rewrite <- Fx.
+unfold f, ex; simpl; unfold cexp; rewrite (mag_mult_bpow _ _ _ Nzx).
+unfold FLT_exp; rewrite <-Z.add_max_distr_r.
+replace (_ - _ + e)%Z with (mag beta x + e - prec)%Z; [ |ring].
+apply Z.max_le_compat_l; lia.
+Qed.
+
 End Fprop_mult_error_FLT.
diff --git a/flocq/Prop/Plus_error.v b/flocq/Prop/Plus_error.v
index 42f80093..514d3aab 100644
--- a/flocq/Prop/Plus_error.v
+++ b/flocq/Prop/Plus_error.v
@@ -50,19 +50,19 @@ destruct (Zle_or_lt e' e) as [He|He].
 exists m.
 unfold F2R at 2. simpl.
 rewrite Rmult_assoc, <- bpow_plus.
-rewrite <- IZR_Zpower. 2: omega.
+rewrite <- IZR_Zpower by lia.
 rewrite <- mult_IZR, Zrnd_IZR...
 unfold F2R. simpl.
 rewrite mult_IZR.
 rewrite Rmult_assoc.
-rewrite IZR_Zpower. 2: omega.
+rewrite IZR_Zpower by lia.
 rewrite <- bpow_plus.
 apply (f_equal (fun v => IZR m * bpow v)%R).
 ring.
 exists ((rnd (IZR m * bpow (e - e'))) * Zpower beta (e' - e))%Z.
 unfold F2R. simpl.
 rewrite mult_IZR.
-rewrite IZR_Zpower. 2: omega.
+rewrite IZR_Zpower by lia.
 rewrite 2!Rmult_assoc.
 rewrite <- 2!bpow_plus.
 apply (f_equal (fun v => _ * bpow v)%R).
@@ -326,8 +326,7 @@ exists (Ztrunc (scaled_mantissa beta fexp x)*Zpower beta (cexp x -e))%Z.
 rewrite Fx at 1; unfold F2R; simpl.
 rewrite mult_IZR, Rmult_assoc.
 f_equal.
-rewrite IZR_Zpower.
-2: omega.
+rewrite IZR_Zpower by lia.
 rewrite <- bpow_plus; f_equal; ring.
 Qed.
 
@@ -351,7 +350,7 @@ case (Zle_or_lt (mag beta (x/IZR beta)) (mag beta y)); intros H1.
 pose (e:=cexp (x / IZR beta)).
 destruct (ex_shift x e) as (nx, Hnx); try exact Fx.
 apply monotone_exp.
-rewrite <- (mag_minus1 x Zx); omega.
+rewrite <- (mag_minus1 x Zx); lia.
 destruct (ex_shift y e) as (ny, Hny); try assumption.
 apply monotone_exp...
 destruct (round_repr_same_exp beta fexp rnd (nx+ny) e) as (n,Hn).
@@ -406,11 +405,11 @@ apply V; left.
 apply lt_mag with beta.
 now apply Rabs_pos_lt.
 rewrite <- mag_minus1 in H1; try assumption.
-rewrite 2!mag_abs; omega.
+rewrite 2!mag_abs; lia.
 (* . *)
 destruct U as [U|U].
 rewrite U; apply Z.le_trans with (mag beta x).
-omega.
+lia.
 rewrite <- mag_abs.
 apply mag_le.
 now apply Rabs_pos_lt.
@@ -424,13 +423,13 @@ now apply Rabs_pos_lt.
 rewrite 2!mag_abs.
 assert (mag beta y < mag beta x - 1)%Z.
 now rewrite (mag_minus1 x Zx).
-omega.
+lia.
 apply cexp_round_ge...
 apply round_plus_neq_0...
 contradict H1; apply Zle_not_lt.
 rewrite <- (mag_minus1 x Zx).
 replace y with (-x)%R.
-rewrite mag_opp; omega.
+rewrite mag_opp; lia.
 lra.
 now exists n.
 Qed.
@@ -520,7 +519,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 omega.
+assert (e + prec < n)%Z; try lia.
 apply lt_bpow with beta.
 apply Rle_lt_trans with (1:=He).
 now apply Hn.
@@ -568,7 +567,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 omega.
+assert (e + prec < n)%Z; try lia.
 apply lt_bpow with beta.
 apply Rle_lt_trans with (1:=He).
 now apply Hn.
diff --git a/flocq/Prop/Relative.v b/flocq/Prop/Relative.v
index 5f87bd84..6b8e8f77 100644
--- a/flocq/Prop/Relative.v
+++ b/flocq/Prop/Relative.v
@@ -147,7 +147,7 @@ apply (lt_bpow beta).
 apply Rle_lt_trans with (2 := proj2 He).
 exact Hx.
 generalize (Hmin ex).
-omega.
+lia.
 apply Rmult_le_compat_l.
 apply bpow_ge_0.
 apply He.
@@ -218,7 +218,7 @@ apply Rle_trans with (bpow (-p + 1) * bpow (ex - 1))%R.
 rewrite <- bpow_plus.
 apply bpow_le.
 generalize (Hmin ex).
-omega.
+lia.
 apply Rmult_le_compat_l.
 apply bpow_ge_0.
 generalize He.
@@ -230,7 +230,7 @@ now apply round_le.
 apply generic_format_bpow.
 ring_simplify (ex - 1 + 1)%Z.
 generalize (Hmin ex).
-omega.
+lia.
 Qed.
 
 Theorem relative_error_round_F2R_emin :
@@ -283,7 +283,7 @@ apply (lt_bpow beta).
 apply Rle_lt_trans with (2 := proj2 He).
 exact Hx.
 generalize (Hmin ex).
-omega.
+lia.
 apply Rmult_le_compat_l.
 apply bpow_ge_0.
 apply He.
@@ -375,7 +375,7 @@ apply Rle_trans with (bpow (-p + 1) * bpow (ex - 1))%R.
 rewrite <- bpow_plus.
 apply bpow_le.
 generalize (Hmin ex).
-omega.
+lia.
 apply Rmult_le_compat_l.
 apply bpow_ge_0.
 generalize He.
@@ -387,7 +387,7 @@ now apply round_le.
 apply generic_format_bpow.
 ring_simplify (ex - 1 + 1)%Z.
 generalize (Hmin ex).
-omega.
+lia.
 Qed.
 
 Theorem relative_error_N_round_F2R_emin :
@@ -425,7 +425,7 @@ Lemma relative_error_FLX_aux :
 Proof.
 intros k.
 unfold FLX_exp.
-omega.
+lia.
 Qed.
 
 Variable rnd : R -> Z.
@@ -505,7 +505,7 @@ Proof.
 unfold u_ro; apply (Rmult_lt_reg_l 2); [lra|].
 rewrite <-Rmult_assoc, Rinv_r, Rmult_1_l, Rmult_1_r; [|lra].
 apply (Rle_lt_trans _ (bpow 0));
-  [apply bpow_le; omega|simpl; lra].
+  [apply bpow_le; lia|simpl; lra].
 Qed.
 
 Lemma u_rod1pu_ro_pos : (0 <= u_ro / (1 + u_ro))%R.
@@ -659,7 +659,7 @@ Proof.
 intros k Hk.
 unfold FLT_exp.
 generalize (Zmax_spec (k - prec) emin).
-omega.
+lia.
 Qed.
 
 Variable rnd : R -> Z.
@@ -843,7 +843,7 @@ destruct relative_error_N_ex with (FLT_exp emin prec) (emin+prec)%Z prec choice
   as (eps,(Heps1,Heps2)).
 now apply FLT_exp_valid.
 intros; unfold FLT_exp.
-rewrite Zmax_left; omega.
+lia.
 rewrite Rabs_right;[assumption|apply Rle_ge; now left].
 exists eps; exists 0%R.
 split;[assumption|split].
@@ -869,14 +869,14 @@ rewrite ulp_neq_0.
 apply bpow_le.
 unfold FLT_exp, cexp.
 rewrite Zmax_right.
-omega.
+lia.
 destruct (mag beta x) as (e,He); simpl.
 assert (e-1 < emin+prec)%Z.
 apply (lt_bpow beta).
 apply Rle_lt_trans with (2:=Hx).
 rewrite <- (Rabs_pos_eq x) by now apply Rlt_le.
 now apply He, Rgt_not_eq.
-omega.
+lia.
 split ; ring.
 Qed.
 
diff --git a/flocq/Prop/Round_odd.v b/flocq/Prop/Round_odd.v
index df2952cc..a433c381 100644
--- a/flocq/Prop/Round_odd.v
+++ b/flocq/Prop/Round_odd.v
@@ -68,7 +68,7 @@ assert (H0:(Zfloor x <= Zfloor y)%Z) by now apply Zfloor_le.
 case (Zle_lt_or_eq _ _  H0); intros H1.
 apply Rle_trans with (1:=Zceil_ub _).
 rewrite Zceil_floor_neq.
-apply IZR_le; omega.
+apply IZR_le; lia.
 now apply sym_not_eq.
 contradict Hy2.
 rewrite <- H1, Hx2; discriminate.
@@ -503,7 +503,7 @@ Proof.
 intros x Hx.
 apply generic_inclusion_mag with fexp; trivial; intros Hx2.
 generalize (fexpe_fexp (mag beta x)).
-omega.
+lia.
 Qed.
 
 
@@ -525,7 +525,7 @@ rewrite Rmult_assoc, <- bpow_plus.
 rewrite <- Hg1; unfold F2R.
 apply f_equal, f_equal.
 ring.
-omega.
+lia.
 split; trivial.
 split.
 unfold canonical, cexp.
@@ -536,7 +536,7 @@ rewrite Z.even_pow.
 rewrite Even_beta.
 apply Bool.orb_true_intro.
 now right.
-omega.
+lia.
 Qed.
 
 
@@ -713,7 +713,7 @@ rewrite Zmult_1_r; apply Rinv_le.
 exact Rlt_0_2.
 apply IZR_le.
 specialize (radix_gt_1 beta).
-omega.
+lia.
 apply Rlt_le_trans with (bpow (fexp e)*1)%R.
 2: right; ring.
 unfold Rdiv; apply Rmult_lt_compat_l.
@@ -766,7 +766,7 @@ rewrite Zplus_comm; unfold Zminus; apply f_equal2.
 rewrite Fexp_Fplus.
 rewrite Z.min_l.
 now rewrite Fexp_d.
-rewrite Hu'2; omega.
+rewrite Hu'2; lia.
 Qed.
 
 Lemma m_eq_0: (0 = F2R d)%R ->  exists f:float beta,
@@ -797,7 +797,7 @@ Lemma fexp_m_eq_0:  (0 = F2R d)%R ->
 Proof with auto with typeclass_instances.
 intros Y.
 assert ((fexp (mag beta (F2R u) - 1) <= fexp (mag beta (F2R u))))%Z.
-2: omega.
+2: lia.
 destruct (mag beta x) as (e,He).
 rewrite Rabs_right in He.
 2: now left.
@@ -812,8 +812,8 @@ ring_simplify (fexp e + 1 - 1)%Z.
 replace (fexp (fexp e)) with (fexp e).
 case exists_NE_; intros V.
 contradict V; rewrite Even_beta; discriminate.
-rewrite (proj2 (V e)); omega.
-apply sym_eq, valid_exp; omega.
+rewrite (proj2 (V e)); lia.
+apply sym_eq, valid_exp; lia.
 Qed.
 
 Lemma Fm:  generic_format beta fexpe m.
@@ -829,7 +829,7 @@ rewrite <- Fexp_d; trivial.
 rewrite Cd.
 unfold cexp.
 generalize (fexpe_fexp (mag beta (F2R d))).
-omega.
+lia.
 (* *)
 destruct m_eq_0 as (g,(Hg1,Hg2)); trivial.
 apply generic_format_F2R' with g.
@@ -838,7 +838,7 @@ intros H; unfold cexp; rewrite Hg2.
 rewrite mag_m_0; try assumption.
 apply Z.le_trans with (1:=fexpe_fexp _).
 generalize (fexp_m_eq_0 Y).
-omega.
+lia.
 Qed.
 
 
@@ -857,7 +857,7 @@ rewrite <- Fexp_d; trivial.
 rewrite Cd.
 unfold cexp.
 generalize (fexpe_fexp  (mag beta (F2R d))).
-omega.
+lia.
 (* *)
 destruct m_eq_0 as (g,(Hg1,Hg2)); trivial.
 apply exists_even_fexp_lt.
@@ -866,7 +866,7 @@ rewrite Hg2.
 rewrite mag_m_0; trivial.
 apply Z.le_lt_trans with (1:=fexpe_fexp _).
 generalize (fexp_m_eq_0 Y).
-omega.
+lia.
 Qed.
 
 
@@ -952,7 +952,7 @@ eexists; split.
 apply sym_eq, Y.
 simpl; unfold cexp.
 apply Z.le_lt_trans with (1:=fexpe_fexp _).
-omega.
+lia.
 absurd (true=false).
 discriminate.
 rewrite <- Hk3, <- Hk'3.
@@ -1105,14 +1105,14 @@ intros _; rewrite Zx, round_0...
 destruct (mag beta x) as (e,He); simpl; intros H.
 apply mag_unique; split.
 apply abs_round_ge_generic...
-apply FLT_format_bpow...
-auto with zarith.
+apply generic_format_FLT_bpow...
+now apply Z.lt_le_pred.
 now apply He.
 assert (V:
   (Rabs (round beta (FLT_exp emin prec) Zrnd_odd x) <= bpow beta e)%R).
 apply abs_round_le_generic...
-apply FLT_format_bpow...
-auto with zarith.
+apply generic_format_FLT_bpow...
+now apply Zlt_le_weak.
 left; now apply He.
 case V; try easy; intros K.
 assert (H0:Rnd_odd_pt beta (FLT_exp emin prec) x (round beta (FLT_exp emin prec) Zrnd_odd x)).
diff --git a/flocq/Prop/Sterbenz.v b/flocq/Prop/Sterbenz.v
index 746b7026..9594ac5d 100644
--- a/flocq/Prop/Sterbenz.v
+++ b/flocq/Prop/Sterbenz.v
@@ -67,7 +67,7 @@ rewrite <- F2R_plus.
 apply generic_format_F2R.
 intros _.
 case_eq (Fplus fx fy).
-intros mxy exy Pxy.
+intros mxy exy Pxy; simpl.
 rewrite <- Pxy, F2R_plus, <- Hx, <- Hy.
 unfold cexp.
 replace exy with (fexp (Z.min ex ey)).
diff --git a/flocq/Version.v b/flocq/Version.v
index d0e36a57..aebb0d76 100644
--- a/flocq/Version.v
+++ b/flocq/Version.v
@@ -29,4 +29,4 @@ Definition Flocq_version := Eval vm_compute in
       parse t major (minor * 10 + N_of_ascii h - N_of_ascii "0"%char)%N
     | Empty_string => (major * 100 + minor)%N
     end in
-  parse "3.1.0"%string N0 N0.
+  parse "3.4.0"%string N0 N0.