Update Flocq to 3.4.0 (#383)

13 files changed, 883 insertions, 241 deletions

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.