Update Flocq to 3.4.0 (#383)

7 files changed, 298 insertions, 277 deletions

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)).