Upgrade to Flocq 2.5.0.

Note: this version of Flocq is compatible with both Coq 8.4 and 8.5.

20 files changed, 2444 insertions, 1078 deletions

diff --git a/flocq/Appli/Fappli_IEEE.v b/flocq/Appli/Fappli_IEEE.v
index 9b5826c1..23999a50 100644
--- a/flocq/Appli/Fappli_IEEE.v
+++ b/flocq/Appli/Fappli_IEEE.v
@@ -48,9 +48,9 @@ Section Binary.
 
 Implicit Arguments exist [[A] [P]].
 
-(** prec is the number of bits of the mantissa including the implicit one
-    emax is the exponent of the infinities
-    Typically p=24 and emax = 128 in single precision *)
+(** [prec] is the number of bits of the mantissa including the implicit one;
+    [emax] is the exponent of the infinities.
+    For instance, binary32 is defined by [prec = 24] and [emax = 128]. *)
 Variable prec emax : Z.
 Context (prec_gt_0_ : Prec_gt_0 prec).
 Hypothesis Hmax : (prec < emax)%Z.
@@ -74,8 +74,7 @@ Definition valid_binary x :=
   end.
 
 (** Basic type used for representing binary FP numbers.
-    Note that there is exactly one such object per FP datum.
-    NaNs do not have any payload. They cannot be distinguished. *)
+    Note that there is exactly one such object per FP datum. *)
 
 Definition nan_pl := {pl | (Zpos (digits2_pos pl) <? prec)%Z  = true}.
 
@@ -382,6 +381,8 @@ Proof.
 now intros [| |? []|].
 Qed.
 
+(** Opposite *)
+
 Definition Bopp opp_nan x :=
   match x with
   | B754_nan sx plx =>
@@ -647,7 +648,8 @@ generalize (prec_gt_0 prec).
 clear -Hmax ; omega.
 Qed.
 
-(** mantissa, round and sticky bits *)
+(** Truncation *)
+
 Record shr_record := { shr_m : Z ; shr_r : bool ; shr_s : bool }.
 
 Definition shr_1 mrs :=
@@ -695,7 +697,7 @@ Qed.
 
 Definition shr mrs e n :=
   match n with
-  | Zpos p => (iter_pos p _ shr_1 mrs, (e + n)%Z)
+  | Zpos p => (iter_pos shr_1 p mrs, (e + n)%Z)
   | _ => (mrs, e)
   end.
 
@@ -746,24 +748,24 @@ destruct n as [|n|n].
 now destruct l as [|[| |]].
 2: now destruct l as [|[| |]].
 unfold shr.
-rewrite iter_nat_of_P.
+rewrite iter_pos_nat.
 rewrite Zpos_eq_Z_of_nat_o_nat_of_P.
 induction (nat_of_P n).
 simpl.
 rewrite Zplus_0_r.
 now destruct l as [|[| |]].
-simpl nat_rect.
+rewrite iter_nat_S.
 rewrite inj_S.
 unfold Zsucc.
-rewrite  Zplus_assoc.
+rewrite Zplus_assoc.
 revert IHn0.
 apply inbetween_shr_1.
 clear -Hm.
 induction n0.
 now destruct l as [|[| |]].
-simpl.
+rewrite iter_nat_S.
 revert IHn0.
-generalize (iter_nat n0 shr_record shr_1 (shr_record_of_loc m l)).
+generalize (iter_nat shr_1 n0 (shr_record_of_loc m l)).
 clear.
 intros (m, r, s) Hm.
 now destruct m as [|[m|m|]|m] ; try (now elim Hm) ; destruct r as [|] ; destruct s as [|].
@@ -827,6 +829,8 @@ intros H.
 now inversion H.
 Qed.
 
+(** Rounding modes *)
+
 Inductive mode := mode_NE | mode_ZR | mode_DN | mode_UP | mode_NA.
 
 Definition round_mode m :=
@@ -927,7 +931,6 @@ destruct (truncate radix2 fexp (Z0, e1, loc_Exact)) as ((m2, e2), l2).
 rewrite shr_m_shr_record_of_loc.
 intros Hm2.
 rewrite Hm2.
-intros z.
 repeat split.
 rewrite Rlt_bool_true.
 repeat split.
@@ -1178,6 +1181,8 @@ destruct x as [sx|sx|sx [plx Hplx]|sx mx ex Hx], y as [sy|sy|sy [ply Hply]|sy my
 apply B2FF_FF2B.
 Qed.
 
+(** Normalization and rounding *)
+
 Definition shl_align mx ex ex' :=
   match (ex' - ex)%Z with
   | Zneg d => (shift_pos d mx, ex')
@@ -1361,6 +1366,7 @@ now apply F2R_lt_0_compat.
 Qed.
 
 (** Addition *)
+
 Definition Bplus plus_nan m x y :=
   let f pl := B754_nan (fst pl) (snd pl) in
   match x, y with
@@ -1475,7 +1481,7 @@ elim Rle_not_lt with (1 := Bz).
 generalize (bounded_lt_emax _ _ Hx) (bounded_lt_emax _ _ Hy) (andb_prop _ _ Hx) (andb_prop _ _ Hy).
 intros Bx By (Hx',_) (Hy',_).
 generalize (canonic_canonic_mantissa sx _ _ Hx') (canonic_canonic_mantissa sy _ _ Hy').
-clear -Bx By Hs.
+clear -Bx By Hs prec_gt_0_.
 intros Cx Cy.
 destruct sx.
 (* ... *)
@@ -1542,6 +1548,8 @@ now apply f_equal.
 apply Sz.
 Qed.
 
+(** Subtraction *)
+
 Definition Bminus minus_nan m x y := Bplus minus_nan m x (Bopp pair y).
 
 Theorem Bminus_correct :
@@ -1571,6 +1579,7 @@ rewrite is_finite_Bopp. auto. now destruct y as [ | | | ].
 Qed.
 
 (** Division *)
+
 Definition Fdiv_core_binary m1 e1 m2 e2 :=
   let d1 := Zdigits2 m1 in
   let d2 := Zdigits2 m2 in
@@ -1737,6 +1746,7 @@ now rewrite B2FF_FF2B.
 Qed.
 
 (** Square root *)
+
 Definition Fsqrt_core_binary m e :=
   let d := Zdigits2 m in
   let s := Zmax (2 * prec - d) 0 in
diff --git a/flocq/Appli/Fappli_IEEE_bits.v b/flocq/Appli/Fappli_IEEE_bits.v
index 5a77bf57..87aa1046 100644
--- a/flocq/Appli/Fappli_IEEE_bits.v
+++ b/flocq/Appli/Fappli_IEEE_bits.v
@@ -617,7 +617,7 @@ apply refl_equal.
 Qed.
 
 Definition default_nan_pl32 : bool * nan_pl 24 :=
-  (false, exist _ (iter_nat 22 _ xO xH) (refl_equal true)).
+  (false, exist _ (iter_nat xO 22 xH) (refl_equal true)).
 
 Definition unop_nan_pl32 (f : binary32) : bool * nan_pl 24 :=
   match f with
@@ -660,7 +660,7 @@ apply refl_equal.
 Qed.
 
 Definition default_nan_pl64 : bool * nan_pl 53 :=
-  (false, exist _ (iter_nat 51 _ xO xH) (refl_equal true)).
+  (false, exist _ (iter_nat xO 51 xH) (refl_equal true)).
 
 Definition unop_nan_pl64 (f : binary64) : bool * nan_pl 53 :=
   match f with
diff --git a/flocq/Appli/Fappli_double_round.v b/flocq/Appli/Fappli_double_round.v
index f83abc47..3ff6c31a 100644
--- a/flocq/Appli/Fappli_double_round.v
+++ b/flocq/Appli/Fappli_double_round.v
@@ -72,12 +72,15 @@ assert (Hx2 : x - round beta fexp1 Zfloor x
               < / 2 * (ulp beta fexp1 x - ulp beta fexp2 x)).
 { now apply (Rplus_lt_reg_r (round beta fexp1 Zfloor x)); ring_simplify. }
 set (x'' := round beta fexp2 (Znearest choice2) x).
-assert (Hr1 : Rabs (x'' - x) <= / 2 * bpow (fexp2 (ln_beta x)));
-  [now unfold x''; apply ulp_half_error|].
+assert (Hr1 : Rabs (x'' - x) <= / 2 * bpow (fexp2 (ln_beta x))).
+apply Rle_trans with (/ 2 * ulp beta fexp2 x).
+now unfold x''; apply error_le_half_ulp...
+rewrite ulp_neq_0;[now right|now apply Rgt_not_eq].
 assert (Pxx' : 0 <= x - x').
 { apply Rle_0_minus.
   apply round_DN_pt.
   exact Vfexp1. }
+rewrite 2!ulp_neq_0 in Hx2; try (apply Rgt_not_eq; assumption).
 assert (Hr2 : Rabs (x'' - x') < / 2 * bpow (fexp1 (ln_beta x))).
 { replace (x'' - x') with (x'' - x + (x - x')) by ring.
   apply (Rle_lt_trans _ _ _ (Rabs_triang _ _)).
@@ -114,6 +117,7 @@ destruct (Req_dec x'' 0) as [Zx''|Nzx''].
                              + (bpow (ln_beta x)
                                 - / 2 * bpow (fexp2 (ln_beta x)))) by ring.
       apply Rplus_le_lt_compat; [exact Hr1|].
+      rewrite ulp_neq_0 in Hx1;[idtac| now apply Rgt_not_eq].
       now rewrite Rabs_right; [|apply Rle_ge; apply Rlt_le].
     - unfold x'' in Nzx'' |- *.
       now apply ln_beta_round_ge; [|apply valid_rnd_N|]. }
@@ -168,12 +172,14 @@ assert (Pxx' : 0 <= x - x').
   apply round_DN_pt.
   exact Vfexp1. }
 assert (x < bpow (ln_beta x) - / 2 * bpow (fexp2 (ln_beta x)));
-  [|now apply double_round_lt_mid_further_place'].
+  [|apply double_round_lt_mid_further_place'; try assumption]...
+2: rewrite ulp_neq_0;[assumption|now apply Rgt_not_eq].
 destruct (Req_dec x' 0) as [Zx'|Nzx'].
 - (* x' = 0 *)
   rewrite Zx' in Hx2; rewrite Rminus_0_r in Hx2.
   apply (Rlt_le_trans _ _ _ Hx2).
   rewrite Rmult_minus_distr_l.
+  rewrite 2!ulp_neq_0;[idtac|now apply Rgt_not_eq|now apply Rgt_not_eq].
   apply Rplus_le_compat_r.
   apply (Rmult_le_reg_r (bpow (- ln_beta x))); [now apply bpow_gt_0|].
   unfold ulp, canonic_exp; bpow_simplify.
@@ -199,7 +205,7 @@ destruct (Req_dec x' 0) as [Zx'|Nzx'].
   { apply (Rplus_le_reg_r (ulp beta fexp1 x)); ring_simplify.
     rewrite <- ulp_DN.
     - change (round _ _ _ _) with x'.
-      apply succ_le_bpow.
+      apply id_p_ulp_le_bpow.
       + exact Px'.
       + change x' with (round beta fexp1 Zfloor x).
         now apply generic_format_round; [|apply valid_rnd_DN].
@@ -210,10 +216,14 @@ destruct (Req_dec x' 0) as [Zx'|Nzx'].
     - exact Vfexp1.
     - exact Px'. }
   fold (canonic_exp beta fexp2 x); fold (ulp beta fexp2 x).
-  assert (/ 2 * ulp beta fexp1 x <= ulp beta fexp1 x); [|lra].
+  assert (/ 2 * ulp beta fexp1 x <= ulp beta fexp1 x).
   rewrite <- (Rmult_1_l (ulp _ _ _)) at 2.
   apply Rmult_le_compat_r; [|lra].
-  apply bpow_ge_0.
+  apply ulp_ge_0.
+  rewrite 2!ulp_neq_0 in Hx2;[|now apply Rgt_not_eq|now apply Rgt_not_eq].
+  rewrite ulp_neq_0 in Hx';[|now apply Rgt_not_eq].
+  rewrite ulp_neq_0 in H;[|now apply Rgt_not_eq].
+  lra.
 Qed.
 
 Lemma double_round_lt_mid_same_place :
@@ -256,7 +266,7 @@ assert (H : Rabs (x * bpow (- fexp1 (ln_beta x)) -
     rewrite <- (Rmult_0_r (/ 2)).
     apply Rmult_lt_compat_l; [lra|].
     apply bpow_gt_0.
-  - exact Hx. }
+  - rewrite ulp_neq_0 in Hx;try apply Rgt_not_eq; assumption. }
 unfold round at 2.
 unfold F2R, scaled_mantissa, canonic_exp; simpl.
 rewrite Hf2f1.
@@ -320,8 +330,10 @@ unfold double_round_eq.
 set (x' := round beta fexp1 Zceil x).
 set (x'' := round beta fexp2 (Znearest choice2) x).
 intros Hx1 Hx2.
-assert (Hr1 : Rabs (x'' - x) <= / 2 * bpow (fexp2 (ln_beta x)));
-  [now unfold x''; apply ulp_half_error|].
+assert (Hr1 : Rabs (x'' - x) <= / 2 * bpow (fexp2 (ln_beta x))).
+  apply Rle_trans with (/2* ulp beta fexp2 x).
+  now unfold x''; apply error_le_half_ulp...
+  rewrite ulp_neq_0;[now right|now apply Rgt_not_eq].
 assert (Px'x : 0 <= x' - x).
 { apply Rle_0_minus.
   apply round_UP_pt.
@@ -335,6 +347,7 @@ assert (Hr2 : Rabs (x'' - x') < / 2 * bpow (fexp1 (ln_beta x))).
   apply Rplus_le_lt_compat.
   - exact Hr1.
   - rewrite Rabs_minus_sym.
+   rewrite 2!ulp_neq_0 in Hx2; try (apply Rgt_not_eq; assumption).
     now rewrite Rabs_right; [|now apply Rle_ge]; apply Hx2. }
 destruct (Req_dec x'' 0) as [Zx''|Nzx''].
 - (* x'' = 0 *)
@@ -382,7 +395,8 @@ destruct (Req_dec x'' 0) as [Zx''|Nzx''].
     apply (Rlt_le_trans _ _ _ Hx2).
     apply Rmult_le_compat_l; [lra|].
     generalize (bpow_ge_0 beta (fexp2 (ln_beta x))).
-    unfold ulp, canonic_exp; lra.
+    rewrite 2!ulp_neq_0; try (apply Rgt_not_eq; assumption).
+    unfold canonic_exp; lra.
   + apply (Rmult_lt_reg_r (bpow (fexp1 (ln_beta x)))); [now apply bpow_gt_0|].
     rewrite <- (Rabs_right (bpow (fexp1 _))) at 1;
       [|now apply Rle_ge; apply bpow_ge_0].
@@ -422,7 +436,7 @@ assert (Hx''pow : x'' = bpow (ln_beta x)).
   { apply Rle_lt_trans with (x + / 2 * ulp beta fexp2 x).
     - apply (Rplus_le_reg_r (- x)); ring_simplify.
       apply Rabs_le_inv.
-      apply ulp_half_error.
+      apply error_le_half_ulp.
       exact Vfexp2.
     - apply Rplus_lt_compat_r.
       rewrite <- Rabs_right at 1; [|now apply Rle_ge; apply Rlt_le].
@@ -442,15 +456,17 @@ assert (Hx''pow : x'' = bpow (ln_beta x)).
   apply (Rlt_le_trans _ _ _ H'x'').
   apply Rplus_le_compat_l.
   rewrite <- (Rmult_1_l (Fcore_Raux.bpow _ _)).
+  rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq].
   apply Rmult_le_compat_r; [now apply bpow_ge_0|].
   lra. }
 assert (Hr : Rabs (x - x'') < / 2 * ulp beta fexp1 x).
 { apply Rle_lt_trans with (/ 2 * ulp beta fexp2 x).
   - rewrite Rabs_minus_sym.
-    apply ulp_half_error.
+    apply error_le_half_ulp.
     exact Vfexp2.
   - apply Rmult_lt_compat_l; [lra|].
-    unfold ulp, canonic_exp; apply bpow_lt.
+    rewrite 2!ulp_neq_0; try now apply Rgt_not_eq.
+    unfold canonic_exp; apply bpow_lt.
     omega. }
 unfold round, F2R, scaled_mantissa, canonic_exp; simpl.
 assert (Hf : (0 <= ln_beta x - fexp1 (ln_beta x''))%Z).
@@ -475,6 +491,7 @@ rewrite (Znearest_imp _ _ (beta ^ (ln_beta x - fexp1 (ln_beta x'')))%Z).
     rewrite <- Rabs_mult.
     rewrite Rmult_minus_distr_r.
     bpow_simplify.
+   rewrite ulp_neq_0 in Hr;[idtac|now apply Rgt_not_eq].
     rewrite <- Hx''pow; exact Hr.
 - rewrite Z2R_Zpower; [|exact Hf].
   apply (Rmult_lt_reg_r (bpow (fexp1 (ln_beta x'')))); [now apply bpow_gt_0|].
@@ -522,7 +539,7 @@ assert (H : Rabs (Z2R (Zceil (x * bpow (- fexp1 (ln_beta x))))
     + apply Rle_0_minus.
       apply round_UP_pt.
       exact Vfexp1.
-  - exact Hx. }
+  -  rewrite ulp_neq_0 in Hx;[exact Hx|now apply Rgt_not_eq]. }
 unfold double_round_eq, round at 2.
 unfold F2R, scaled_mantissa, canonic_exp; simpl.
 rewrite Hf2f1.
@@ -761,9 +778,10 @@ destruct (Req_dec y 0) as [Zy|Nzy].
 - (* y = 0 *)
   now rewrite Zy; rewrite Rplus_0_r.
 - (* y <> 0 *)
-  apply (ln_beta_succ beta fexp); [assumption|assumption|].
+  apply (ln_beta_plus_eps beta fexp); [assumption|assumption|].
   split; [assumption|].
-  unfold ulp, canonic_exp.
+  rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq].
+  unfold canonic_exp.
   destruct (ln_beta y) as (ey, Hey); simpl in *.
   apply Rlt_le_trans with (bpow ey).
   + now rewrite <- (Rabs_right y); [apply Hey|apply Rle_ge].
@@ -797,8 +815,7 @@ apply ln_beta_unique.
 split.
 - apply Rabs_ge; right.
   assert (Hy : y < ulp beta fexp (bpow (ln_beta x - 1))).
-  { unfold ulp, canonic_exp.
-    rewrite ln_beta_bpow.
+  { rewrite ulp_bpow.
     replace (_ + _)%Z with (ln_beta x : Z) by ring.
     rewrite <- (Rabs_right y); [|now apply Rle_ge; apply Rlt_le].
     apply Rlt_le_trans with (bpow (ln_beta y)).
@@ -808,7 +825,8 @@ split.
   apply Rle_trans with (bpow (ln_beta x - 1)
                         + ulp beta fexp (bpow (ln_beta x - 1))).
   + now apply Rplus_le_compat_l; apply Rlt_le.
-  + apply succ_le_lt; [|exact Fx|now split; [apply bpow_gt_0|]].
+  + rewrite <- succ_eq_pos;[idtac|apply bpow_ge_0].
+    apply succ_le_lt; [apply Vfexp|idtac|exact Fx|assumption].
     apply (generic_format_bpow beta fexp (ln_beta x - 1)).
     replace (_ + _)%Z with (ln_beta x : Z) by ring.
     assert (fexp (ln_beta x) < ln_beta x)%Z; [|omega].
@@ -1039,13 +1057,15 @@ apply double_round_lt_mid.
   apply (Rlt_le_trans _ _ _ (proj2 (double_round_plus_aux1_aux 2 P2 fexp1 x y Px
                                                                Py Hly Lxy Fx))).
   ring_simplify.
-  unfold ulp, canonic_exp; rewrite Lxy.
+  rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq, Rplus_lt_0_compat].
+  unfold canonic_exp; rewrite Lxy.
   apply (Rmult_le_reg_r (bpow (- fexp1 (ln_beta x)))); [now apply bpow_gt_0|].
   bpow_simplify.
   apply (Rle_trans _ _ _ Bpow2).
   rewrite <- (Rmult_1_r (/ 2)) at 3.
   apply Rmult_le_compat_l; lra.
-- unfold ulp, round, F2R, scaled_mantissa, canonic_exp; simpl; rewrite Lxy.
+- rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq, Rplus_lt_0_compat].
+  unfold round, F2R, scaled_mantissa, canonic_exp; simpl; rewrite Lxy.
   intro Hf2'.
   apply (Rmult_lt_reg_r (bpow (- fexp1 (ln_beta x))));
     [now apply bpow_gt_0|].
@@ -1056,7 +1076,8 @@ apply double_round_lt_mid.
   apply (Rlt_le_trans _ _ _ (proj2 (double_round_plus_aux1_aux 2 P2 fexp1 x y Px
                                                                Py Hly Lxy Fx))).
   apply (Rmult_le_reg_r (bpow (- fexp1 (ln_beta x)))); [now apply bpow_gt_0|].
-  unfold ulp, canonic_exp; rewrite Lxy, Rmult_minus_distr_r; bpow_simplify.
+  rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq, Rplus_lt_0_compat].
+  unfold canonic_exp; rewrite Lxy, Rmult_minus_distr_r; bpow_simplify.
   apply (Rle_trans _ _ _ Bpow2).
   rewrite <- (Rmult_1_r (/ 2)) at 3; rewrite <- Rmult_minus_distr_l.
   apply Rmult_le_compat_l; [lra|].
@@ -1391,7 +1412,8 @@ apply double_round_gt_mid.
     [now apply double_round_minus_aux2_aux; try assumption; omega|].
     apply (Rlt_le_trans _ _ _ Ly).
     now apply bpow_le.
-  + unfold ulp, canonic_exp.
+  + rewrite ulp_neq_0;[idtac|now apply sym_not_eq, Rlt_not_eq, Rgt_minus].
+    unfold canonic_exp.
     replace (_ - 2)%Z with (fexp1 (ln_beta (x - y)) - 1 - 1)%Z by ring.
     unfold Zminus at 1; rewrite bpow_plus.
     rewrite Rmult_comm.
@@ -1423,7 +1445,8 @@ apply double_round_gt_mid.
   + unfold Fcore_Raux.bpow, Z.pow_pos; simpl.
     rewrite Zmult_1_r; apply Rinv_le; [lra|].
     now change 2 with (Z2R 2); apply Z2R_le.
-  + unfold ulp, canonic_exp.
+  + rewrite 2!ulp_neq_0; try now apply Rgt_not_eq, Rgt_minus.
+    unfold canonic_exp.
     apply (Rplus_le_reg_r (bpow (fexp2 (ln_beta (x - y))))); ring_simplify.
     apply Rle_trans with (2 * bpow (fexp1 (ln_beta (x - y)) - 1)).
     * rewrite Rmult_plus_distr_r; rewrite Rmult_1_l.
@@ -1868,19 +1891,22 @@ apply double_round_lt_mid.
   apply (Rlt_le_trans _ _ _ (proj2 (double_round_plus_aux1_aux 1 P1 fexp1 x y Px
                                                                Py Hly Lxy Fx))).
   ring_simplify.
-  unfold ulp, canonic_exp; rewrite Lxy.
+  rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq, Rplus_lt_0_compat].
+  unfold canonic_exp; rewrite Lxy.
   apply (Rmult_le_reg_r (bpow (- fexp1 (ln_beta x))));
     [now apply bpow_gt_0|].
   bpow_simplify.
   apply (Rle_trans _ _ _ Bpow3); lra.
-- unfold ulp, round, F2R, scaled_mantissa, canonic_exp; simpl; rewrite Lxy.
+- rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq, Rplus_lt_0_compat].
+  unfold round, F2R, scaled_mantissa, canonic_exp; simpl; rewrite Lxy.
   intro Hf2'.
   unfold midp.
   apply (Rplus_lt_reg_r (- round beta fexp1 Zfloor (x + y))); ring_simplify.
   rewrite <- Rmult_minus_distr_l.
   apply (Rlt_le_trans _ _ _ (proj2 (double_round_plus_aux1_aux 1 P1 fexp1 x y Px
                                                                Py Hly Lxy Fx))).
-  unfold ulp, canonic_exp; rewrite Lxy.
+  rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq, Rplus_lt_0_compat].
+  unfold canonic_exp; rewrite Lxy.
   apply (Rmult_le_reg_r (bpow (- fexp1 (ln_beta x))));
     [now apply bpow_gt_0|].
   rewrite (Rmult_assoc (/ 2)).
@@ -2106,7 +2132,8 @@ apply double_round_gt_mid.
     [now apply double_round_minus_aux2_aux|].
     apply (Rlt_le_trans _ _ _ Ly).
     now apply bpow_le.
-  + unfold ulp, canonic_exp.
+  + rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq, Rgt_minus].
+    unfold canonic_exp.
     unfold Zminus at 1; rewrite bpow_plus.
     rewrite Rmult_comm.
     apply Rmult_le_compat_r; [now apply bpow_ge_0|].
@@ -2124,7 +2151,8 @@ apply double_round_gt_mid.
   apply (Rlt_le_trans _ _ _ Ly).
   apply Rle_trans with (bpow (fexp1 (ln_beta (x - y)) - 1));
     [now apply bpow_le|].
-  unfold ulp, canonic_exp.
+  rewrite 2!ulp_neq_0; try now apply Rgt_not_eq, Rgt_minus.
+  unfold canonic_exp.
   apply (Rmult_le_reg_r (bpow (- fexp1 (ln_beta (x - y)))));
     [now apply bpow_gt_0|].
   rewrite Rmult_assoc.
@@ -2533,7 +2561,7 @@ destruct (generic_format_EM beta fexp1 x) as [Fx|Nfx].
   now apply (generic_inclusion_ln_beta beta fexp1); [omega|].
 - (* ~ generic_format beta fexp1 x *)
   assert (Hceil : round beta fexp1 Zceil x = rd + u1);
-  [now apply ulp_DN_UP|].
+  [now apply round_UP_DN_ulp|].
   assert (Hf2' : (fexp2 (ln_beta x) <= fexp1 (ln_beta x) - 1)%Z); [omega|].
   destruct (Rlt_or_le (x - rd) (/ 2 * (u1 - u2))).
   + (* x - rd < / 2 * (u1 - u2) *)
@@ -2589,10 +2617,11 @@ assert (Hbeta : (2 <= beta)%Z).
 { destruct beta as (beta_val,beta_prop).
   now apply Zle_bool_imp_le. }
 set (a := round beta fexp1 Zfloor (sqrt x)).
-set (u1 := ulp beta fexp1 (sqrt x)).
-set (u2 := ulp beta fexp2 (sqrt x)).
+set (u1 := bpow (fexp1 (ln_beta (sqrt x)))).
+set (u2 := bpow (fexp2 (ln_beta (sqrt x)))).
 set (b := / 2 * (u1 - u2)).
 set (b' := / 2 * (u1 + u2)).
+unfold midp; rewrite 2!ulp_neq_0; try now apply Rgt_not_eq, sqrt_lt_R0.
 apply Rnot_ge_lt; intro H; apply Rge_le in H.
 assert (Fa : generic_format beta fexp1 a).
 { unfold a.
@@ -2619,7 +2648,7 @@ assert (Pb : 0 < b).
   rewrite <- (Rmult_0_r (/ 2)).
   apply Rmult_lt_compat_l; [lra|].
   apply Rlt_Rminus.
-  unfold u2, u1, ulp, canonic_exp.
+  unfold u2, u1.
   apply bpow_lt.
   omega. }
 assert (Pb' : 0 < b').
@@ -2686,7 +2715,7 @@ destruct (Req_dec a 0) as [Za|Nza].
 - (* a <> 0 *)
   assert (Pa : 0 < a); [lra|].
   assert (Hla : (ln_beta a = ln_beta (sqrt x) :> Z)).
-  { unfold a; apply ln_beta_round_DN.
+  { unfold a; apply ln_beta_DN.
     - exact Vfexp1.
     - now fold a. }
   assert (Hl' : 0 < - (u2 * a) + b * b).
@@ -2697,12 +2726,14 @@ destruct (Req_dec a 0) as [Za|Nza].
     replace (_ / 8) with (/ 4 * (u2 ^ 2 + u1 ^ 2)) by field.
     apply Rlt_le_trans with (u2 * bpow (ln_beta (sqrt x))).
     - apply Rmult_lt_compat_l; [now unfold u2, ulp; apply bpow_gt_0|].
-      unfold u1, ulp, canonic_exp; rewrite <- Hla.
-      apply Rlt_le_trans with (a + ulp beta fexp1 a).
+      unfold u1; rewrite <- Hla.
+      apply Rlt_le_trans with (a + bpow (fexp1 (ln_beta a))).
       + apply Rplus_lt_compat_l.
-        rewrite <- (Rmult_1_l (ulp _ _ _)).
+        rewrite <- (Rmult_1_l (bpow _)) at 2.
         apply Rmult_lt_compat_r; [apply bpow_gt_0|lra].
-      + apply (succ_le_bpow _ _ _ _ Pa Fa).
+      + apply Rle_trans with (a+ ulp beta fexp1 a).
+        right; now rewrite ulp_neq_0.
+        apply (id_p_ulp_le_bpow _ _ _ _ Pa Fa).
         apply Rabs_lt_inv, bpow_ln_beta_gt.
     - apply Rle_trans with (bpow (- 2) * u1 ^ 2).
       + unfold pow; rewrite Rmult_1_r.
@@ -2745,9 +2776,10 @@ destruct (Req_dec a 0) as [Za|Nza].
     apply Rlt_le_trans with (bpow (ln_beta (sqrt x)) * u2).
     - apply Rmult_lt_compat_r; [now unfold u2, ulp; apply bpow_gt_0|].
       apply Rlt_le_trans with (a + u1); [lra|].
-      unfold u1.
-      rewrite <- ulp_DN; [|exact Vfexp1|exact Pa]; fold a.
-      apply succ_le_bpow.
+      unfold u1; fold (canonic_exp beta fexp1 (sqrt x)).
+      rewrite <- canonic_exp_DN; [|exact Vfexp1|exact Pa]; fold a.
+      rewrite <- ulp_neq_0; trivial.
+      apply id_p_ulp_le_bpow.
       + exact Pa.
       + now apply round_DN_pt.
       + apply Rle_lt_trans with (sqrt x).
@@ -2782,21 +2814,6 @@ destruct (Req_dec a 0) as [Za|Nza].
   + now apply Rle_trans with x.
 Qed.
 
-(* --> Fcore_Raux *)
-Lemma sqrt_neg : forall x, x <= 0 -> sqrt x = 0.
-Proof.
-intros x Npx.
-destruct (Req_dec x 0) as [Zx|Nzx].
-- (* x = 0 *)
-  rewrite Zx.
-  exact sqrt_0.
-- (* x < 0 *)
-  unfold sqrt.
-  destruct Rcase_abs.
-  + reflexivity.
-  + casetype False.
-    now apply Nzx, Rle_antisym; [|apply Rge_le].
-Qed.
 
 Lemma double_round_sqrt :
   forall fexp1 fexp2 : Z -> Z,
@@ -3028,10 +3045,11 @@ Lemma double_round_sqrt_beta_ge_4_aux :
 Proof.
 intros Hbeta fexp1 fexp2 Vfexp1 Vfexp2 Hexp x Px Hf2 Fx.
 set (a := round beta fexp1 Zfloor (sqrt x)).
-set (u1 := ulp beta fexp1 (sqrt x)).
-set (u2 := ulp beta fexp2 (sqrt x)).
+set (u1 := bpow (fexp1 (ln_beta (sqrt x)))).
+set (u2 := bpow (fexp2 (ln_beta (sqrt x)))).
 set (b := / 2 * (u1 - u2)).
 set (b' := / 2 * (u1 + u2)).
+unfold midp; rewrite 2!ulp_neq_0; try now apply Rgt_not_eq, sqrt_lt_R0.
 apply Rnot_ge_lt; intro H; apply Rge_le in H.
 assert (Fa : generic_format beta fexp1 a).
 { unfold a.
@@ -3125,7 +3143,7 @@ destruct (Req_dec a 0) as [Za|Nza].
 - (* a <> 0 *)
   assert (Pa : 0 < a); [lra|].
   assert (Hla : (ln_beta a = ln_beta (sqrt x) :> Z)).
-  { unfold a; apply ln_beta_round_DN.
+  { unfold a; apply ln_beta_DN.
     - exact Vfexp1.
     - now fold a. }
   assert (Hl' : 0 < - (u2 * a) + b * b).
@@ -3136,12 +3154,13 @@ destruct (Req_dec a 0) as [Za|Nza].
     replace (_ / 8) with (/ 4 * (u2 ^ 2 + u1 ^ 2)) by field.
     apply Rlt_le_trans with (u2 * bpow (ln_beta (sqrt x))).
     - apply Rmult_lt_compat_l; [now unfold u2, ulp; apply bpow_gt_0|].
-      unfold u1, ulp, canonic_exp; rewrite <- Hla.
+      unfold u1; rewrite <- Hla.
       apply Rlt_le_trans with (a + ulp beta fexp1 a).
       + apply Rplus_lt_compat_l.
         rewrite <- (Rmult_1_l (ulp _ _ _)).
+        rewrite ulp_neq_0; trivial.
         apply Rmult_lt_compat_r; [apply bpow_gt_0|lra].
-      + apply (succ_le_bpow _ _ _ _ Pa Fa).
+      + apply (id_p_ulp_le_bpow _ _ _ _ Pa Fa).
         apply Rabs_lt_inv, bpow_ln_beta_gt.
     - apply Rle_trans with (bpow (- 1) * u1 ^ 2).
       + unfold pow; rewrite Rmult_1_r.
@@ -3184,9 +3203,10 @@ destruct (Req_dec a 0) as [Za|Nza].
     apply Rlt_le_trans with (bpow (ln_beta (sqrt x)) * u2).
     - apply Rmult_lt_compat_r; [now unfold u2, ulp; apply bpow_gt_0|].
       apply Rlt_le_trans with (a + u1); [lra|].
-      unfold u1.
-      rewrite <- ulp_DN; [|exact Vfexp1|exact Pa]; fold a.
-      apply succ_le_bpow.
+      unfold u1; fold (canonic_exp beta fexp1 (sqrt x)).
+      rewrite <- canonic_exp_DN; [|exact Vfexp1|exact Pa]; fold a.
+      rewrite <- ulp_neq_0; trivial.
+      apply id_p_ulp_le_bpow.
       + exact Pa.
       + now apply round_DN_pt.
       + apply Rle_lt_trans with (sqrt x).
@@ -3504,9 +3524,11 @@ assert (Hf : F2R f = x).
   rewrite (Rmult_assoc _ (Z2R n)).
   rewrite Rinv_r;
     [rewrite Rmult_1_r|change 0 with (Z2R 0); apply Z2R_neq; omega].
-  simpl; fold (canonic_exp beta fexp1 x); fold (ulp beta fexp1 x); fold u.
-  rewrite Xmid at 2.
+  simpl; fold (canonic_exp beta fexp1 x).
+  rewrite <- 2!ulp_neq_0; try now apply Rgt_not_eq.
+  fold u; rewrite Xmid at 2.
   apply f_equal2; [|reflexivity].
+  rewrite ulp_neq_0; try now apply Rgt_not_eq.
   destruct (Req_dec rd 0) as [Zrd|Nzrd].
   - (* rd = 0 *)
     rewrite Zrd.
@@ -3657,7 +3679,7 @@ split.
   replace (bpow _) with (bpow (ln_beta x) - / 2 * u2 + / 2 * u2) by ring.
   apply Rplus_lt_le_compat; [exact Hx|].
   apply Rabs_le_inv.
-  now apply ulp_half_error.
+  now apply error_le_half_ulp.
 Qed.
 
 Lemma double_round_all_mid_cases :
@@ -3714,7 +3736,7 @@ destruct (Ztrichotomy (ln_beta x) (fexp1 (ln_beta x) - 1)) as [Hlt|[Heq|Hgt]].
           now apply (generic_inclusion_ln_beta beta fexp1); [omega|].
         - (* ~ generic_format beta fexp1 x *)
           assert (Hceil : round beta fexp1 Zceil x = x' + u1);
-          [now apply ulp_DN_UP|].
+          [now apply round_UP_DN_ulp|].
           assert (Hf2' : (fexp2 (ln_beta x) <= fexp1 (ln_beta x) - 1)%Z);
             [omega|].
           assert (midp' fexp1 x + / 2 * ulp beta fexp2 x < x);
@@ -3769,12 +3791,15 @@ assert (Hfx : (fexp1 (ln_beta x) < ln_beta x)%Z);
 assert (Hfy : (fexp1 (ln_beta y) < ln_beta y)%Z);
   [now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]|].
 set (p := bpow (ln_beta (x / y))).
-set (u2 := ulp beta fexp2 (x / y)).
+set (u2 := bpow (fexp2 (ln_beta (x / y)))).
 revert Fx Fy.
 unfold generic_format, F2R, scaled_mantissa, canonic_exp; simpl.
 set (mx := Ztrunc (x * bpow (- fexp1 (ln_beta x)))).
 set (my := Ztrunc (y * bpow (- fexp1 (ln_beta y)))).
 intros Fx Fy.
+rewrite ulp_neq_0.
+2: apply Rmult_integral_contrapositive_currified; [now apply Rgt_not_eq|idtac].
+2: now apply Rinv_neq_0_compat, Rgt_not_eq.
 intro Hl.
 assert (Hr : x / y < p);
   [now apply Rabs_lt_inv; apply bpow_ln_beta_gt|].
@@ -3903,6 +3928,9 @@ assert (Hfx : (fexp1 (ln_beta x) < ln_beta x)%Z);
   [now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]|].
 assert (Hfy : (fexp1 (ln_beta y) < ln_beta y)%Z);
   [now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]|].
+assert (S : (x / y <> 0)%R).
+apply Rmult_integral_contrapositive_currified; [now apply Rgt_not_eq|idtac].
+now apply Rinv_neq_0_compat, Rgt_not_eq.
 cut (~ (/ 2 * (ulp beta fexp1 (x / y) - ulp beta fexp2 (x / y))
         <= x / y - round beta fexp1 Zfloor (x / y)
         < / 2 * ulp beta fexp1 (x / y))).
@@ -3913,9 +3941,10 @@ cut (~ (/ 2 * (ulp beta fexp1 (x / y) - ulp beta fexp2 (x / y))
   - apply (Rplus_lt_reg_l (round beta fexp1 Zfloor (x / y))).
     ring_simplify.
     apply H'. }
-set (u1 := ulp beta fexp1 (x / y)).
-set (u2 := ulp beta fexp2 (x / y)).
+set (u1 := bpow (fexp1 (ln_beta (x / y)))).
+set (u2 := bpow (fexp2 (ln_beta (x / y)))).
 set (x' := round beta fexp1 Zfloor (x / y)).
+rewrite 2!ulp_neq_0; trivial.
 revert Fx Fy.
 unfold generic_format, F2R, scaled_mantissa, canonic_exp; simpl.
 set (mx := Ztrunc (x * bpow (- fexp1 (ln_beta x)))).
@@ -4098,9 +4127,13 @@ cut (~ (/ 2 * ulp beta fexp1 (x / y)
   - apply (Rplus_le_reg_l (round beta fexp1 Zfloor (x / y))).
     ring_simplify.
     apply H'. }
-set (u1 := ulp beta fexp1 (x / y)).
-set (u2 := ulp beta fexp2 (x / y)).
+set (u1 := bpow (fexp1 (ln_beta (x / y)))).
+set (u2 := bpow (fexp2 (ln_beta (x / y)))).
 set (x' := round beta fexp1 Zfloor (x / y)).
+assert (S : (x / y <> 0)%R).
+apply Rmult_integral_contrapositive_currified; [now apply Rgt_not_eq|idtac].
+now apply Rinv_neq_0_compat, Rgt_not_eq.
+rewrite 2!ulp_neq_0; trivial.
 revert Fx Fy.
 unfold generic_format, F2R, scaled_mantissa, canonic_exp; simpl.
 set (mx := Ztrunc (x * bpow (- fexp1 (ln_beta x)))).
diff --git a/flocq/Appli/Fappli_rnd_odd.v b/flocq/Appli/Fappli_rnd_odd.v
index b3244589..4741047f 100644
--- a/flocq/Appli/Fappli_rnd_odd.v
+++ b/flocq/Appli/Fappli_rnd_odd.v
@@ -356,6 +356,80 @@ simpl; ring.
 apply Rgt_not_eq, bpow_gt_0.
 Qed.
 
+
+
+Theorem Rnd_odd_pt_unicity :
+  forall x f1 f2 : R,
+  Rnd_odd_pt x f1 -> Rnd_odd_pt x f2 ->
+  f1 = f2.
+Proof.
+intros x f1 f2 (Ff1,H1) (Ff2,H2).
+(* *)
+case (generic_format_EM beta fexp x); intros L.
+apply trans_eq with x.
+case H1; try easy.
+intros (J,_); case J; intros J'.
+apply Rnd_DN_pt_idempotent with format; assumption.
+apply Rnd_UP_pt_idempotent with format; assumption.
+case H2; try easy.
+intros (J,_); case J; intros J'; apply sym_eq.
+apply Rnd_DN_pt_idempotent with format; assumption.
+apply Rnd_UP_pt_idempotent with format; assumption.
+(* *)
+destruct H1 as [H1|(H1,H1')].
+contradict L; now rewrite <- H1.
+destruct H2 as [H2|(H2,H2')].
+contradict L; now rewrite <- H2.
+destruct H1 as [H1|H1]; destruct H2 as [H2|H2].
+apply Rnd_DN_pt_unicity with format x; assumption.
+destruct H1' as (ff,(K1,(K2,K3))).
+destruct H2' as (gg,(L1,(L2,L3))).
+absurd (true = false); try discriminate.
+rewrite <- L3.
+apply trans_eq with (negb (Zeven (Fnum ff))).
+rewrite K3; easy.
+apply sym_eq.
+generalize (DN_UP_parity_generic beta fexp).
+unfold DN_UP_parity_prop; intros T; apply (T x); clear T; try assumption...
+rewrite <- K1; apply Rnd_DN_pt_unicity with (generic_format beta fexp) x; try easy...
+now apply round_DN_pt...
+rewrite <- L1; apply Rnd_UP_pt_unicity with (generic_format beta fexp) x; try easy...
+now apply round_UP_pt...
+(* *)
+destruct H1' as (ff,(K1,(K2,K3))).
+destruct H2' as (gg,(L1,(L2,L3))).
+absurd (true = false); try discriminate.
+rewrite <- K3.
+apply trans_eq with (negb (Zeven (Fnum gg))).
+rewrite L3; easy.
+apply sym_eq.
+generalize (DN_UP_parity_generic beta fexp).
+unfold DN_UP_parity_prop; intros T; apply (T x); clear T; try assumption...
+rewrite <- L1; apply Rnd_DN_pt_unicity with (generic_format beta fexp) x; try easy...
+now apply round_DN_pt...
+rewrite <- K1; apply Rnd_UP_pt_unicity with (generic_format beta fexp) x; try easy...
+now apply round_UP_pt...
+apply Rnd_UP_pt_unicity with format x; assumption.
+Qed.
+
+
+
+Theorem Rnd_odd_pt_monotone :
+  round_pred_monotone (Rnd_odd_pt).
+Proof with auto with typeclass_instances.
+intros x y f g H1 H2 Hxy.
+apply Rle_trans with (round beta fexp Zrnd_odd x).
+right; apply Rnd_odd_pt_unicity with x; try assumption.
+apply round_odd_pt.
+apply Rle_trans with (round beta fexp Zrnd_odd y).
+apply round_le...
+right; apply Rnd_odd_pt_unicity with y; try assumption.
+apply round_odd_pt.
+Qed.
+
+
+
+
 End Fcore_rnd_odd.
 
 Section Odd_prop_aux.
@@ -462,7 +536,7 @@ Lemma ln_beta_d:  (0< F2R d)%R ->
     (ln_beta beta (F2R d) = ln_beta beta x :>Z).
 Proof with auto with typeclass_instances.
 intros Y.
-rewrite d_eq; apply ln_beta_round_DN...
+rewrite d_eq; apply ln_beta_DN...
 now rewrite <- d_eq.
 Qed.
 
@@ -861,13 +935,9 @@ case K2; clear K2; intros K2.
 case (Rle_or_lt  x m); intros Y;[destruct Y|idtac].
 (* . *)
 apply trans_eq with (F2R d).
-apply round_N_DN_betw with (F2R u)...
+apply round_N_eq_DN_pt with (F2R u)...
 apply DN_odd_d_aux; split; try left; assumption.
 apply UP_odd_d_aux; split; try left; assumption.
-split.
-apply round_ge_generic...
-apply generic_format_fexpe_fexp, Hd.
-apply Hd.
 assert (o <= (F2R d + F2R u) / 2)%R.
 apply round_le_generic...
 apply Fm.
@@ -876,10 +946,7 @@ destruct H1; trivial.
 apply P.
 now apply Rlt_not_eq.
 trivial.
-apply sym_eq, round_N_DN_betw with (F2R u)...
-split.
-apply Hd.
-exact H0.
+apply sym_eq, round_N_eq_DN_pt with (F2R u)...
 (* . *)
 replace o with x.
 reflexivity.
@@ -887,10 +954,9 @@ apply sym_eq, round_generic...
 rewrite H0; apply Fm.
 (* . *)
 apply trans_eq with (F2R u).
-apply round_N_UP_betw with (F2R d)...
+apply round_N_eq_UP_pt with (F2R d)...
 apply DN_odd_d_aux; split; try left; assumption.
 apply UP_odd_d_aux; split; try left; assumption.
-split.
 assert ((F2R d + F2R u) / 2 <= o)%R.
 apply round_ge_generic...
 apply Fm.
@@ -899,13 +965,7 @@ destruct H0; trivial.
 apply P.
 now apply Rgt_not_eq.
 rewrite <- H0; trivial.
-apply round_le_generic...
-apply generic_format_fexpe_fexp, Hu.
-apply Hu.
-apply sym_eq, round_N_UP_betw with (F2R d)...
-split.
-exact Y.
-apply Hu.
+apply sym_eq, round_N_eq_UP_pt with (F2R d)...
 Qed.
 
 
diff --git a/flocq/Core/Fcore_FIX.v b/flocq/Core/Fcore_FIX.v
index a3b8d4d0..e224a64a 100644
--- a/flocq/Core/Fcore_FIX.v
+++ b/flocq/Core/Fcore_FIX.v
@@ -22,6 +22,7 @@ Require Import Fcore_Raux.
 Require Import Fcore_defs.
 Require Import Fcore_rnd.
 Require Import Fcore_generic_fmt.
+Require Import Fcore_ulp.
 Require Import Fcore_rnd_ne.
 
 Section RND_FIX.
@@ -84,4 +85,16 @@ intros ex ey H.
 apply Zle_refl.
 Qed.
 
+Theorem ulp_FIX: forall x, ulp beta FIX_exp x = bpow emin.
+Proof.
+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.
+intros n _; reflexivity.
+reflexivity.
+Qed.
+
+
 End RND_FIX.
diff --git a/flocq/Core/Fcore_FLT.v b/flocq/Core/Fcore_FLT.v
index 273ff69f..372af6ad 100644
--- a/flocq/Core/Fcore_FLT.v
+++ b/flocq/Core/Fcore_FLT.v
@@ -25,6 +25,7 @@ Require Import Fcore_generic_fmt.
 Require Import Fcore_float_prop.
 Require Import Fcore_FLX.
 Require Import Fcore_FIX.
+Require Import Fcore_ulp.
 Require Import Fcore_rnd_ne.
 
 Section RND_FLT.
@@ -222,7 +223,6 @@ Theorem generic_format_FLT_FIX :
   generic_format beta (FIX_exp emin) x ->
   generic_format beta FLT_exp x.
 Proof with auto with typeclass_instances.
-clear prec_gt_0_.
 apply generic_inclusion_le...
 intros e He.
 unfold FIX_exp.
@@ -231,6 +231,75 @@ omega.
 apply Zle_refl.
 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.
+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 Zle_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 canonic_exp, FLT_exp.
+apply Z.max_r.
+assert (ln_beta beta x-1 < emin+prec)%Z;[idtac|omega].
+destruct (ln_beta beta x) as (e,He); simpl.
+apply lt_bpow with beta.
+apply Rle_lt_trans with (2:=Hx).
+now apply He.
+Qed.
+
+Theorem ulp_FLT_le: forall x, (bpow (emin+prec) <= Rabs x)%R ->
+  (ulp beta FLT_exp x <= Rabs x * bpow (1-prec))%R.
+Proof.
+intros x Hx.
+assert (x <> 0)%R.
+intros Z; contradict Hx; apply Rgt_not_le, Rlt_gt.
+rewrite Z, Rabs_R0; apply bpow_gt_0.
+rewrite ulp_neq_0; try assumption.
+unfold canonic_exp, FLT_exp.
+destruct (ln_beta beta x) as (e,He).
+apply Rle_trans with (bpow (e-1)*bpow (1-prec))%R.
+rewrite <- bpow_plus.
+right; apply f_equal.
+apply trans_eq with (e-prec)%Z;[idtac|ring].
+simpl; apply Z.max_l.
+assert (emin+prec <= e)%Z; try omega.
+apply le_bpow with beta.
+apply Rle_trans with (1:=Hx).
+left; now apply He.
+apply Rmult_le_compat_r.
+apply bpow_ge_0.
+now apply He.
+Qed.
+
+
+Theorem ulp_FLT_ge: forall x, (Rabs x * bpow (-prec) < ulp beta FLT_exp x)%R.
+Proof.
+intros x; case (Req_dec x 0); intros Hx.
+rewrite Hx, ulp_FLT_small, Rabs_R0, Rmult_0_l; try apply bpow_gt_0.
+rewrite Rabs_R0; apply bpow_gt_0.
+rewrite ulp_neq_0; try exact Hx.
+unfold canonic_exp, FLT_exp.
+apply Rlt_le_trans with (bpow (ln_beta beta x)*bpow (-prec))%R.
+apply Rmult_lt_compat_r.
+apply bpow_gt_0.
+now apply bpow_ln_beta_gt.
+rewrite <- bpow_plus.
+apply bpow_le.
+apply Z.le_max_l.
+Qed.
+
+
+
 (** FLT is a nice format: it has a monotone exponent... *)
 Global Instance FLT_exp_monotone : Monotone_exp FLT_exp.
 Proof.
diff --git a/flocq/Core/Fcore_FLX.v b/flocq/Core/Fcore_FLX.v
index 800540f2..55f6db61 100644
--- a/flocq/Core/Fcore_FLX.v
+++ b/flocq/Core/Fcore_FLX.v
@@ -24,6 +24,7 @@ Require Import Fcore_rnd.
 Require Import Fcore_generic_fmt.
 Require Import Fcore_float_prop.
 Require Import Fcore_FIX.
+Require Import Fcore_ulp.
 Require Import Fcore_rnd_ne.
 
 Section RND_FLX.
@@ -211,6 +212,43 @@ now apply FLXN_format_generic.
 now apply generic_format_FLXN.
 Qed.
 
+Theorem ulp_FLX_0: (ulp beta FLX_exp 0 = 0)%R.
+Proof.
+unfold ulp; rewrite Req_bool_true; trivial.
+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.
+Qed.
+
+Theorem ulp_FLX_le: forall x, (ulp beta FLX_exp x <= Rabs x * bpow (1-prec))%R.
+Proof.
+intros x; case (Req_dec x 0); intros Hx.
+rewrite Hx, ulp_FLX_0, Rabs_R0.
+right; ring.
+rewrite ulp_neq_0; try exact Hx.
+unfold canonic_exp, FLX_exp.
+replace (ln_beta beta x - prec)%Z with ((ln_beta beta x - 1) + (1-prec))%Z by ring.
+rewrite bpow_plus.
+apply Rmult_le_compat_r.
+apply bpow_ge_0.
+now apply bpow_ln_beta_le.
+Qed.
+
+
+Theorem ulp_FLX_ge: forall x, (Rabs x * bpow (-prec) <= ulp beta FLX_exp x)%R.
+Proof.
+intros x; case (Req_dec x 0); intros Hx.
+rewrite Hx, ulp_FLX_0, Rabs_R0.
+right; ring.
+rewrite ulp_neq_0; try exact Hx.
+unfold canonic_exp, FLX_exp.
+unfold Zminus; rewrite bpow_plus.
+apply Rmult_le_compat_r.
+apply bpow_ge_0.
+left; now apply bpow_ln_beta_gt.
+Qed.
+
 (** FLX is a nice format: it has a monotone exponent... *)
 Global Instance FLX_exp_monotone : Monotone_exp FLX_exp.
 Proof.
diff --git a/flocq/Core/Fcore_FTZ.v b/flocq/Core/Fcore_FTZ.v
index 5f3e5337..2ebc7851 100644
--- a/flocq/Core/Fcore_FTZ.v
+++ b/flocq/Core/Fcore_FTZ.v
@@ -23,6 +23,7 @@ Require Import Fcore_defs.
 Require Import Fcore_rnd.
 Require Import Fcore_generic_fmt.
 Require Import Fcore_float_prop.
+Require Import Fcore_ulp.
 Require Import Fcore_FLX.
 
 Section RND_FTZ.
@@ -182,7 +183,6 @@ Theorem FTZ_format_FLXN :
   (bpow (emin + prec - 1) <= Rabs x)%R ->
   FLXN_format beta prec x -> FTZ_format x.
 Proof.
-clear prec_gt_0_.
 intros x Hx Fx.
 apply FTZ_format_generic.
 apply generic_format_FLXN in Fx.
@@ -195,6 +195,21 @@ apply Zle_refl.
 omega.
 Qed.
 
+Theorem ulp_FTZ_0: ulp beta FTZ_exp 0 = bpow (emin+prec-1).
+Proof with auto with typeclass_instances.
+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.
+assert (V:(FTZ_exp (emin+prec-1) = emin+prec-1)%Z).
+unfold FTZ_exp; rewrite Zlt_bool_true; omega.
+intros n H2; rewrite <-V.
+apply f_equal, fexp_negligible_exp_eq...
+omega.
+Qed.
+
+
 Section FTZ_round.
 
 (** Rounding with FTZ *)
diff --git a/flocq/Core/Fcore_Raux.v b/flocq/Core/Fcore_Raux.v
index 3758324f..d728e0ba 100644
--- a/flocq/Core/Fcore_Raux.v
+++ b/flocq/Core/Fcore_Raux.v
@@ -207,6 +207,27 @@ rewrite 3!(Rmult_comm r).
 now apply Rmult_min_distr_r.
 Qed.
 
+Lemma Rmin_opp: forall x y, (Rmin (-x) (-y) = - Rmax x y)%R.
+Proof.
+intros x y.
+apply Rmax_case_strong; intros H.
+rewrite Rmin_left; trivial.
+now apply Ropp_le_contravar.
+rewrite Rmin_right; trivial.
+now apply Ropp_le_contravar.
+Qed.
+
+Lemma Rmax_opp: forall x y, (Rmax (-x) (-y) = - Rmin x y)%R.
+Proof.
+intros x y.
+apply Rmin_case_strong; intros H.
+rewrite Rmax_left; trivial.
+now apply Ropp_le_contravar.
+rewrite Rmax_right; trivial.
+now apply Ropp_le_contravar.
+Qed.
+
+
 Theorem exp_le :
   forall x y : R,
   (x <= y)%R -> (exp x <= exp y)%R.
@@ -1930,6 +1951,16 @@ destruct (ln_beta x) as (ex, Ex) ; simpl.
 now apply Ex.
 Qed.
 
+Theorem bpow_ln_beta_le :
+  forall x, (x <> 0)%R ->
+    (bpow (ln_beta x-1) <= Rabs x)%R.
+Proof.
+intros x Hx.
+destruct (ln_beta x) as (ex, Ex) ; simpl.
+now apply Ex.
+Qed.
+
+
 Theorem ln_beta_le_Zpower :
   forall m e,
   m <> Z0 ->
@@ -2306,6 +2337,160 @@ Qed.
 
 End cond_Ropp.
 
+
+(** LPO taken from Coquelicot *)
+
+Theorem LPO_min :
+  forall P : nat -> Prop, (forall n, P n \/ ~ P n) ->
+  {n : nat | P n /\ forall i, (i < n)%nat -> ~ P i} + {forall n, ~ P n}.
+Proof.
+assert (Hi: forall n, (0 < INR n + 1)%R).
+  intros N.
+  rewrite <- S_INR.
+  apply lt_0_INR.
+  apply lt_0_Sn.
+intros P HP.
+set (E y := exists n, (P n /\ y = / (INR n + 1))%R \/ (~ P n /\ y = 0)%R).
+assert (HE: forall n, P n -> E (/ (INR n + 1))%R).
+  intros n Pn.
+  exists n.
+  left.
+  now split.
+assert (BE: is_upper_bound E 1).
+  intros x [y [[_ ->]|[_ ->]]].
+  rewrite <- Rinv_1 at 2.
+  apply Rinv_le.
+  exact Rlt_0_1.
+  rewrite <- S_INR.
+  apply (le_INR 1), le_n_S, le_0_n.
+  exact Rle_0_1.
+destruct (completeness E) as [l [ub lub]].
+  now exists 1%R.
+  destruct (HP O) as [H0|H0].
+  exists 1%R.
+  exists O.
+  left.
+  apply (conj H0).
+  rewrite Rplus_0_l.
+  apply sym_eq, Rinv_1.
+  exists 0%R.
+  exists O.
+  right.
+  now split.
+destruct (Rle_lt_dec l 0) as [Hl|Hl].
+  right.
+  intros n Pn.
+  apply Rle_not_lt with (1 := Hl).
+  apply Rlt_le_trans with (/ (INR n + 1))%R.
+  now apply Rinv_0_lt_compat.
+  apply ub.
+  now apply HE.
+left.
+set (N := Zabs_nat (up (/l) - 2)).
+exists N.
+assert (HN: (INR N + 1 = IZR (up (/ l)) - 1)%R).
+  unfold N.
+  rewrite INR_IZR_INZ.
+  rewrite inj_Zabs_nat.
+  replace (IZR (up (/ l)) - 1)%R with (IZR (up (/ l) - 2) + 1)%R.
+  apply (f_equal (fun v => IZR v + 1)%R).
+  apply Zabs_eq.
+  apply Zle_minus_le_0.
+  apply (Zlt_le_succ 1).
+  apply lt_IZR.
+  apply Rle_lt_trans with (/l)%R.
+  apply Rmult_le_reg_r with (1 := Hl).
+  rewrite Rmult_1_l, Rinv_l by now apply Rgt_not_eq.
+  apply lub.
+  exact BE.
+  apply archimed.
+  rewrite minus_IZR.
+  simpl.
+  ring.
+assert (H: forall i, (i < N)%nat -> ~ P i).
+  intros i HiN Pi.
+  unfold is_upper_bound in ub.
+  refine (Rle_not_lt _ _ (ub (/ (INR i + 1))%R _) _).
+  now apply HE.
+  rewrite <- (Rinv_involutive l) by now apply Rgt_not_eq.
+  apply Rinv_1_lt_contravar.
+  rewrite <- S_INR.
+  apply (le_INR 1).
+  apply le_n_S.
+  apply le_0_n.
+  apply Rlt_le_trans with (INR N + 1)%R.
+  apply Rplus_lt_compat_r.
+  now apply lt_INR.
+  rewrite HN.
+  apply Rplus_le_reg_r with (-/l + 1)%R.
+  ring_simplify.
+  apply archimed.
+destruct (HP N) as [PN|PN].
+  now split.
+elimtype False.
+refine (Rle_not_lt _ _ (lub (/ (INR (S N) + 1))%R _) _).
+  intros x [y [[Py ->]|[_ ->]]].
+  destruct (eq_nat_dec y N) as [HyN|HyN].
+  elim PN.
+  now rewrite <- HyN.
+  apply Rinv_le.
+  apply Hi.
+  apply Rplus_le_compat_r.
+  apply Rnot_lt_le.
+  intros Hy.
+  refine (H _ _ Py).
+  apply INR_lt in Hy.
+  clear -Hy HyN.
+  omega.
+  now apply Rlt_le, Rinv_0_lt_compat.
+rewrite S_INR, HN.
+ring_simplify (IZR (up (/ l)) - 1 + 1)%R.
+rewrite <- (Rinv_involutive l) at 2 by now apply Rgt_not_eq.
+apply Rinv_1_lt_contravar.
+rewrite <- Rinv_1.
+apply Rinv_le.
+exact Hl.
+now apply lub.
+apply archimed.
+Qed.
+
+Theorem LPO :
+  forall P : nat -> Prop, (forall n, P n \/ ~ P n) ->
+  {n : nat | P n} + {forall n, ~ P n}.
+Proof.
+intros P HP.
+destruct (LPO_min P HP) as [[n [Pn _]]|Pn].
+left.
+now exists n.
+now right.
+Qed.
+
+
+Lemma LPO_Z : forall P : Z -> Prop, (forall n, P n \/ ~P n) ->
+  {n : Z| P n} + {forall n, ~ P n}.
+Proof.
+intros P H.
+destruct (LPO (fun n => P (Z.of_nat n))) as [J|J].
+intros n; apply H.
+destruct J as (n, Hn).
+left; now exists (Z.of_nat n).
+destruct (LPO (fun n => P (-Z.of_nat n)%Z)) as [K|K].
+intros n; apply H.
+destruct K as (n, Hn).
+left; now exists (-Z.of_nat n)%Z.
+right; intros n; case (Zle_or_lt 0 n); intros M.
+rewrite <- (Zabs_eq n); trivial.
+rewrite <- Zabs2Nat.id_abs.
+apply J.
+rewrite <- (Zopp_involutive n).
+rewrite <- (Z.abs_neq n).
+rewrite <- Zabs2Nat.id_abs.
+apply K.
+omega.
+Qed.
+
+
+
 (** A little tactic to simplify terms of the form [bpow a * bpow b]. *)
 Ltac bpow_simplify :=
   (* bpow ex * bpow ey ~~> bpow (ex + ey) *)
diff --git a/flocq/Core/Fcore_Zaux.v b/flocq/Core/Fcore_Zaux.v
index 4702d62e..f6731b4c 100644
--- a/flocq/Core/Fcore_Zaux.v
+++ b/flocq/Core/Fcore_Zaux.v
@@ -927,3 +927,65 @@ intros [|a|a] [|b|b] ; try rewrite Zpos_div_eucl_aux_correct ; easy.
 Qed.
 
 End faster_div.
+
+Section Iter.
+
+Context {A : Type}.
+Variable (f : A -> A).
+
+Fixpoint iter_nat (n : nat) (x : A) {struct n} : A :=
+  match n with
+  | S n' => iter_nat n' (f x)
+  | O => x
+  end.
+
+Lemma iter_nat_plus :
+  forall (p q : nat) (x : A),
+  iter_nat (p + q) x = iter_nat p (iter_nat q x).
+Proof.
+induction q.
+now rewrite plus_0_r.
+intros x.
+rewrite <- plus_n_Sm.
+apply IHq.
+Qed.
+
+Lemma iter_nat_S :
+  forall (p : nat) (x : A),
+  iter_nat (S p) x = f (iter_nat p x).
+Proof.
+induction p.
+easy.
+simpl.
+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.
+Proof.
+induction p ; intros x.
+rewrite Pos2Nat.inj_xI.
+simpl.
+rewrite plus_0_r.
+rewrite iter_nat_plus.
+rewrite (IHp (f x)).
+apply IHp.
+rewrite Pos2Nat.inj_xO.
+simpl.
+rewrite plus_0_r.
+rewrite iter_nat_plus.
+rewrite (IHp x).
+apply IHp.
+easy.
+Qed.
+
+End Iter.
diff --git a/flocq/Core/Fcore_digits.v b/flocq/Core/Fcore_digits.v
index 13174d29..d40c1a09 100644
--- a/flocq/Core/Fcore_digits.v
+++ b/flocq/Core/Fcore_digits.v
@@ -21,7 +21,7 @@ Require Import ZArith.
 Require Import Zquot.
 Require Import Fcore_Zaux.
 
-(** Computes the number of bits (radix 2) of a positive integer.
+(** Number of bits (radix 2) of a positive integer.
 
 It serves as an upper bound on the number of digits to ensure termination.
 *)
@@ -466,6 +466,8 @@ now apply Hd.
 now rewrite 3!Zdigit_lt.
 Qed.
 
+(** Left and right shifts *)
+
 Definition Zscale n k :=
   if Zle_bool 0 k then (n * Zpower beta k)%Z else Z.quot n (Zpower beta (-k)).
 
@@ -545,6 +547,8 @@ rewrite Zle_bool_true with (1 := Hk).
 now apply Zscale_mul_pow.
 Qed.
 
+(** Slice of an integer *)
+
 Definition Zslice n k1 k2 :=
   if Zle_bool 0 k2 then Z.rem (Zscale n (-k1)) (Zpower beta k2) else Z0.
 
@@ -756,6 +760,7 @@ Fixpoint Zdigits_aux (nb pow : Z) (n : nat) { struct n } : Z :=
 End digits_aux.
 
 (** Number of digits of an integer *)
+
 Definition Zdigits n :=
   match n with
   | Z0 => Z0
@@ -1011,7 +1016,7 @@ generalize (Zpower_gt_Zdigits e x).
 omega.
 Qed.
 
-(** Characterizes the number digits of a product.
+(** Number of digits of a product.
 
 This strong version is needed for proofs of division and square root
 algorithms, since they involve operation remainders.
@@ -1126,6 +1131,8 @@ Qed.
 
 End Fcore_digits.
 
+(** Specialized version for computing the number of bits of an integer *)
+
 Section Zdigits2.
 
 Theorem Z_of_nat_S_digits2_Pnat :
diff --git a/flocq/Core/Fcore_float_prop.v b/flocq/Core/Fcore_float_prop.v
index e1535bc9..8199ede6 100644
--- a/flocq/Core/Fcore_float_prop.v
+++ b/flocq/Core/Fcore_float_prop.v
@@ -233,6 +233,37 @@ rewrite <- F2R_0 with (Fexp f).
 now apply F2R_lt_compat.
 Qed.
 
+Theorem F2R_neq_0_compat :
+ forall f : float beta,
+  (Fnum f <> 0)%Z ->
+  (F2R f <> 0)%R.
+Proof.
+intros f H H1.
+apply H.
+now apply F2R_eq_0_reg with (Fexp f).
+Qed.
+
+
+Lemma Fnum_ge_0_compat: forall (f : float beta),
+  (0 <= F2R f)%R -> (0 <= Fnum f)%Z.
+Proof.
+intros f H.
+case (Zle_or_lt 0 (Fnum f)); trivial.
+intros H1; contradict H.
+apply Rlt_not_le.
+now apply F2R_lt_0_compat.
+Qed.
+
+Lemma Fnum_le_0_compat: forall (f : float beta),
+  (F2R f <= 0)%R -> (Fnum f <= 0)%Z.
+Proof.
+intros f H.
+case (Zle_or_lt (Fnum f) 0); trivial.
+intros H1; contradict H.
+apply Rlt_not_le.
+now apply F2R_gt_0_compat.
+Qed.
+
 (** Floats and bpow *)
 Theorem F2R_bpow :
   forall e : Z,
diff --git a/flocq/Core/Fcore_generic_fmt.v b/flocq/Core/Fcore_generic_fmt.v
index 45729f2a..bac65b9d 100644
--- a/flocq/Core/Fcore_generic_fmt.v
+++ b/flocq/Core/Fcore_generic_fmt.v
@@ -1015,7 +1015,7 @@ Qed.
 
 End monotone.
 
-Theorem round_abs_abs' :
+Theorem round_abs_abs :
   forall P : R -> R -> Prop,
   ( forall rnd (Hr : Valid_rnd rnd) x, (0 <= x)%R -> P x (round rnd x) ) ->
   forall rnd {Hr : Valid_rnd rnd} x, P (Rabs x) (Rabs (round rnd x)).
@@ -1043,18 +1043,6 @@ apply round_le...
 now apply Rlt_le.
 Qed.
 
-(* TODO: remove *)
-Theorem round_abs_abs :
-  forall P : R -> R -> Prop,
-  ( forall rnd (Hr : Valid_rnd rnd) x, P x (round rnd x) ) ->
-  forall rnd {Hr : Valid_rnd rnd} x, P (Rabs x) (Rabs (round rnd x)).
-Proof.
-intros P HP.
-apply round_abs_abs'.
-intros.
-now apply HP.
-Qed.
-
 Theorem round_bounded_large :
   forall rnd {Hr : Valid_rnd rnd} x ex,
   (fexp ex < ex)%Z ->
@@ -1064,7 +1052,7 @@ Proof with auto with typeclass_instances.
 intros rnd Hr x ex He.
 apply round_abs_abs...
 clear rnd Hr x.
-intros rnd' Hr x.
+intros rnd' Hr x _.
 apply round_bounded_large_pos...
 Qed.
 
@@ -1076,7 +1064,7 @@ Proof.
 intros rnd Hr x ex H1 H2.
 generalize Rabs_R0.
 rewrite <- H2 at 1.
-apply (round_abs_abs' (fun t rt => forall (ex : Z),
+apply (round_abs_abs (fun t rt => forall (ex : Z),
 (bpow (ex - 1) <= t < bpow ex)%R ->
 rt = 0%R -> (ex <= fexp ex)%Z)); trivial.
 clear; intros rnd Hr x Hx.
@@ -1496,7 +1484,7 @@ right.
 now rewrite Zmax_l with (1 := Zlt_le_weak _ _ He).
 Qed.
 
-Theorem ln_beta_round_DN :
+Theorem ln_beta_DN :
   forall x,
   (0 < round Zfloor x)%R ->
   (ln_beta beta (round Zfloor x) = ln_beta beta x :> Z).
@@ -1513,7 +1501,6 @@ now apply Rgt_not_eq.
 now apply Rlt_le.
 Qed.
 
-(* TODO: remove *)
 Theorem canonic_exp_DN :
   forall x,
   (0 < round Zfloor x)%R ->
@@ -1521,7 +1508,7 @@ Theorem canonic_exp_DN :
 Proof.
 intros x Hd.
 apply (f_equal fexp).
-now apply ln_beta_round_DN.
+now apply ln_beta_DN.
 Qed.
 
 Theorem scaled_mantissa_DN :
@@ -2312,7 +2299,7 @@ intros x Gx.
 apply generic_format_abs_inv.
 apply generic_format_abs in Gx.
 revert rnd valid_rnd x Gx.
-refine (round_abs_abs' _ (fun x y => generic_format fexp1 x -> generic_format fexp1 y) _).
+refine (round_abs_abs _ (fun x y => generic_format fexp1 x -> generic_format fexp1 y) _).
 intros rnd valid_rnd x [Hx|Hx] Gx.
 (* x > 0 *)
 generalize (ln_beta_generic_gt _ x (Rgt_not_eq _ _ Hx) Gx).
diff --git a/flocq/Core/Fcore_rnd.v b/flocq/Core/Fcore_rnd.v
index 94c94203..171c27fc 100644
--- a/flocq/Core/Fcore_rnd.v
+++ b/flocq/Core/Fcore_rnd.v
@@ -39,7 +39,7 @@ exists f.
 intros g Hg.
 now apply H2 with (3 := Rle_refl x).
 (* . *)
-exists (projT1 (completeness _ H3 H1)).
+exists (proj1_sig (completeness _ H3 H1)).
 destruct completeness as (f1, (H4, H5)).
 simpl.
 destruct H1 as (f2, H1).
@@ -58,7 +58,7 @@ Theorem round_fun_of_pred :
   { f : R -> R | forall x, rnd x (f x) }.
 Proof.
 intros rnd H.
-exists (fun x => projT1 (round_val_of_pred rnd H x)).
+exists (fun x => proj1_sig (round_val_of_pred rnd H x)).
 intros x.
 now destruct round_val_of_pred as (f, H1).
 Qed.
diff --git a/flocq/Core/Fcore_rnd_ne.v b/flocq/Core/Fcore_rnd_ne.v
index 6829c0c8..1f265406 100644
--- a/flocq/Core/Fcore_rnd_ne.v
+++ b/flocq/Core/Fcore_rnd_ne.v
@@ -164,7 +164,7 @@ now apply Rlt_le.
 assert (Hxe2 : (fexp (ex + 1) <= ex)%Z) by now apply valid_exp.
 assert (Hud: (F2R xu = F2R xd + ulp beta fexp x)%R).
 rewrite Hxu, Hxd.
-now apply ulp_DN_UP.
+now apply round_UP_DN_ulp.
 destruct (total_order_T (bpow ex) (F2R xu)) as [[Hu2|Hu2]|Hu2].
 (* - xu > bpow ex  *)
 elim (Rlt_not_le _ _ Hu2).
@@ -191,7 +191,8 @@ rewrite Rmult_plus_distr_r.
 rewrite Z2R_Zpower, <- bpow_plus.
 ring_simplify (ex - fexp ex + fexp ex)%Z.
 rewrite Hu2, Hud.
-unfold ulp, canonic_exp.
+rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq].
+unfold canonic_exp.
 rewrite ln_beta_unique with beta x ex.
 unfold F2R.
 simpl. ring.
@@ -223,7 +224,8 @@ specialize (H ex).
 omega.
 (* - xu < bpow ex *)
 revert Hud.
-unfold ulp, F2R.
+rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq].
+unfold F2R.
 rewrite Hd, Hu.
 unfold canonic_exp.
 rewrite ln_beta_unique with beta (F2R xu) ex.
diff --git a/flocq/Core/Fcore_ulp.v b/flocq/Core/Fcore_ulp.v
index 04bed01c..1c27de31 100644
--- a/flocq/Core/Fcore_ulp.v
+++ b/flocq/Core/Fcore_ulp.v
@@ -32,9 +32,79 @@ Notation bpow e := (bpow beta e).
 
 Variable fexp : Z -> Z.
 
+(** Definition and basic properties about the minimal exponent, when it exists *)
+
+Lemma Z_le_dec_aux: forall x y : Z, (x <= y)%Z \/ ~ (x <= y)%Z.
+intros.
+destruct (Z_le_dec x y).
+now left.
+now right.
+Qed.
+
+
+(** [negligible_exp] is either none (as in FLX) or Some n such that n <= fexp n. *)
+Definition negligible_exp: option Z :=
+  match (LPO_Z _ (fun z => Z_le_dec_aux z (fexp z))) with
+   | inleft N => Some (proj1_sig N)
+   | inright _ => None
+ end.
+
+
+Inductive negligible_exp_prop: option Z -> Prop :=
+  | negligible_None: (forall n, (fexp n < n)%Z) -> negligible_exp_prop None
+  | negligible_Some: forall n, (n <= fexp n)%Z -> negligible_exp_prop (Some n).
+
+
+Lemma negligible_exp_spec: negligible_exp_prop negligible_exp.
+Proof.
+unfold negligible_exp; destruct LPO_Z as [(n,Hn)|Hn].
+now apply negligible_Some.
+apply negligible_None.
+intros n; specialize (Hn n); omega.
+Qed.
+
+Lemma negligible_exp_spec': (negligible_exp = None /\ forall n, (fexp n < n)%Z)
+           \/ exists n, (negligible_exp = Some n /\ (n <= fexp n)%Z).
+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.
+Qed.
+
 Context { valid_exp : Valid_exp fexp }.
 
-Definition ulp x := bpow (canonic_exp beta fexp x).
+Lemma fexp_negligible_exp_eq: forall n m, (n <= fexp n)%Z -> (m <= fexp m)%Z -> fexp n = fexp m.
+Proof.
+intros n m Hn Hm.
+case (Zle_or_lt n m); intros H.
+apply valid_exp; omega.
+apply sym_eq, valid_exp; omega.
+Qed.
+
+
+(** Definition and basic properties about the ulp *)
+(** Now includes a nice ulp(0): ulp(0) is now 0 when there is no minimal
+   exponent, such as in FLX, and beta^(fexp n) when there is a n such
+   that n <= fexp n. For instance, the value of ulp(O) is then
+   beta^emin in FIX and FLT. The main lemma to use is ulp_neq_0 that
+   is equivalent to the previous "unfold ulp" provided the value is
+   not zero. *)
+
+Definition ulp x := match Req_bool x 0 with
+  | true   => match negligible_exp with
+            | Some n => bpow (fexp n)
+            | None => 0%R
+            end
+  | false  => bpow (canonic_exp beta fexp x)
+ end.
+
+Lemma ulp_neq_0 : forall x:R, (x <> 0)%R -> ulp x = bpow (canonic_exp beta fexp x).
+Proof.
+intros  x Hx.
+unfold ulp; case (Req_bool_spec x); trivial.
+intros H; now contradict H.
+Qed.
 
 Notation F := (generic_format beta fexp).
 
@@ -43,17 +113,37 @@ Theorem ulp_opp :
 Proof.
 intros x.
 unfold ulp.
+case Req_bool_spec; intros H1.
+rewrite Req_bool_true; trivial.
+rewrite <- (Ropp_involutive x), H1; ring.
+rewrite Req_bool_false.
 now rewrite canonic_exp_opp.
+intros H2; apply H1; rewrite H2; ring.
 Qed.
 
 Theorem ulp_abs :
   forall x, ulp (Rabs x) = ulp x.
 Proof.
 intros x.
-unfold ulp.
+unfold ulp; case (Req_bool_spec x 0); intros H1.
+rewrite Req_bool_true; trivial.
+now rewrite H1, Rabs_R0.
+rewrite Req_bool_false.
 now rewrite canonic_exp_abs.
+now apply Rabs_no_R0.
 Qed.
 
+Theorem ulp_ge_0:
+  forall x, (0 <= ulp x)%R.
+Proof.
+intros x; unfold ulp; case Req_bool_spec; intros.
+case negligible_exp; intros.
+apply bpow_ge_0.
+apply Rle_refl.
+apply bpow_ge_0.
+Qed.
+
+
 Theorem ulp_le_id:
   forall x,
     (0 < x)%R ->
@@ -63,7 +153,9 @@ Proof.
 intros x Zx Fx.
 rewrite <- (Rmult_1_l (ulp x)).
 pattern x at 2; rewrite Fx.
-unfold F2R, ulp; simpl.
+rewrite ulp_neq_0.
+2: now apply Rgt_not_eq.
+unfold F2R; simpl.
 apply Rmult_le_compat_r.
 apply bpow_ge_0.
 replace 1%R with (Z2R (Zsucc 0)) by reflexivity.
@@ -86,12 +178,15 @@ now apply Rabs_pos_lt.
 now apply generic_format_abs.
 Qed.
 
-Theorem ulp_DN_UP :
+
+(* was ulp_DN_UP *)
+Theorem round_UP_DN_ulp :
   forall x, ~ F x ->
   round beta fexp Zceil x = (round beta fexp Zfloor x + ulp x)%R.
 Proof.
 intros x Fx.
-unfold round, ulp. simpl.
+rewrite ulp_neq_0.
+unfold round. simpl.
 unfold F2R. simpl.
 rewrite Zceil_floor_neq.
 rewrite Z2R_plus. simpl.
@@ -103,459 +198,233 @@ rewrite <- H.
 rewrite Ztrunc_Z2R.
 rewrite H.
 now rewrite scaled_mantissa_mult_bpow.
+intros V; apply Fx.
+rewrite V.
+apply generic_format_0.
 Qed.
 
-(** The successor of x is x + ulp x *)
-Theorem succ_le_bpow :
-  forall x e, (0 < x)%R -> F x ->
-  (x < bpow e)%R ->
-  (x + ulp x <= bpow e)%R.
-Proof.
-intros x e Zx Fx Hx.
-pattern x at 1 ; rewrite Fx.
-unfold ulp, F2R. simpl.
-pattern (bpow (canonic_exp beta fexp x)) at 2 ; rewrite <- Rmult_1_l.
-rewrite <- Rmult_plus_distr_r.
-change 1%R with (Z2R 1).
-rewrite <- Z2R_plus.
-change (F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x) + 1) (canonic_exp beta fexp x)) <= bpow e)%R.
-apply F2R_p1_le_bpow.
-apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
-now rewrite <- Fx.
-now rewrite <- Fx.
-Qed.
 
-Theorem ln_beta_succ :
-  forall x, (0 < x)%R -> F x ->
-  forall eps, (0 <= eps < ulp x)%R ->
-  ln_beta beta (x + eps) = ln_beta beta x :> Z.
-Proof.
-intros x Zx Fx eps Heps.
-destruct (ln_beta beta x) as (ex, He).
-simpl.
-specialize (He (Rgt_not_eq _ _ Zx)).
-apply ln_beta_unique.
+Theorem ulp_bpow :
+  forall e, ulp (bpow e) = bpow (fexp (e + 1)).
+intros e.
+rewrite ulp_neq_0.
+apply f_equal.
+apply canonic_exp_fexp.
 rewrite Rabs_pos_eq.
-rewrite Rabs_pos_eq in He.
 split.
-apply Rle_trans with (1 := proj1 He).
-pattern x at 1 ; rewrite <- Rplus_0_r.
-now apply Rplus_le_compat_l.
-apply Rlt_le_trans with (x + ulp x)%R.
-now apply Rplus_lt_compat_l.
-pattern x at 1 ; rewrite Fx.
-unfold ulp, F2R. simpl.
-pattern (bpow (canonic_exp beta fexp x)) at 2 ; rewrite <- Rmult_1_l.
-rewrite <- Rmult_plus_distr_r.
-change 1%R with (Z2R 1).
-rewrite <- Z2R_plus.
-change (F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x) + 1) (canonic_exp beta fexp x)) <= bpow ex)%R.
-apply F2R_p1_le_bpow.
-apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
-now rewrite <- Fx.
-now rewrite <- Fx.
-now apply Rlt_le.
-apply Rplus_le_le_0_compat.
-now apply Rlt_le.
-apply Heps.
+ring_simplify (e + 1 - 1)%Z.
+apply Rle_refl.
+apply bpow_lt.
+apply Zlt_succ.
+apply bpow_ge_0.
+apply Rgt_not_eq, Rlt_gt, bpow_gt_0.
 Qed.
 
-Theorem round_DN_succ :
-  forall x, (0 < x)%R -> F x ->
-  forall eps, (0 <= eps < ulp x)%R ->
-  round beta fexp Zfloor (x + eps) = x.
+
+Lemma generic_format_ulp_0:
+  F (ulp 0).
 Proof.
-intros x Zx Fx eps Heps.
-pattern x at 2 ; rewrite Fx.
-unfold round.
-unfold scaled_mantissa. simpl.
-unfold canonic_exp at 1 2.
-rewrite ln_beta_succ ; trivial.
-apply (f_equal (fun m => F2R (Float beta m _))).
-rewrite Ztrunc_floor.
-apply Zfloor_imp.
-split.
-apply (Rle_trans _ _ _ (Zfloor_lb _)).
-apply Rmult_le_compat_r.
-apply bpow_ge_0.
-pattern x at 1 ; rewrite <- Rplus_0_r.
-now apply Rplus_le_compat_l.
-apply Rlt_le_trans with ((x + ulp x) * bpow (- canonic_exp beta fexp x))%R.
-apply Rmult_lt_compat_r.
-apply bpow_gt_0.
-now apply Rplus_lt_compat_l.
-rewrite Rmult_plus_distr_r.
-rewrite Z2R_plus.
-apply Rplus_le_compat.
-pattern x at 1 3 ; rewrite Fx.
-unfold F2R. simpl.
-rewrite Rmult_assoc.
-rewrite <- bpow_plus.
-rewrite Zplus_opp_r.
-rewrite Rmult_1_r.
-rewrite Zfloor_Z2R.
-apply Rle_refl.
 unfold ulp.
-rewrite <- bpow_plus.
-rewrite Zplus_opp_r.
-apply Rle_refl.
-apply Rmult_le_pos.
-now apply Rlt_le.
-apply bpow_ge_0.
+rewrite Req_bool_true; trivial.
+case negligible_exp_spec.
+intros _; apply generic_format_0.
+intros n H1.
+apply generic_format_bpow.
+now apply valid_exp.
 Qed.
 
-Theorem generic_format_succ :
-  forall x, (0 < x)%R -> F x ->
-  F (x + ulp x).
+Lemma generic_format_bpow_ge_ulp_0:  forall e,
+    (ulp 0 <= bpow e)%R -> F (bpow e).
 Proof.
-intros x Zx Fx.
-destruct (ln_beta beta x) as (ex, Ex).
-specialize (Ex (Rgt_not_eq _ _ Zx)).
-assert (Ex' := Ex).
-rewrite Rabs_pos_eq in Ex'.
-destruct (succ_le_bpow x ex) ; try easy.
-unfold generic_format, scaled_mantissa, canonic_exp.
-rewrite ln_beta_unique with beta (x + ulp x)%R ex.
-pattern x at 1 3 ; rewrite Fx.
-unfold ulp, scaled_mantissa.
-rewrite canonic_exp_fexp with (1 := Ex).
-unfold F2R. simpl.
-rewrite Rmult_plus_distr_r.
-rewrite Rmult_assoc.
-rewrite <- bpow_plus, Zplus_opp_r, Rmult_1_r.
-change (bpow 0) with (Z2R 1).
-rewrite <- Z2R_plus.
-rewrite Ztrunc_Z2R.
-rewrite Z2R_plus.
-rewrite Rmult_plus_distr_r.
-now rewrite Rmult_1_l.
-rewrite Rabs_pos_eq.
-split.
-apply Rle_trans with (1 := proj1 Ex').
-pattern x at 1 ; rewrite <- Rplus_0_r.
-apply Rplus_le_compat_l.
-apply bpow_ge_0.
-exact H.
-apply Rplus_le_le_0_compat.
-now apply Rlt_le.
-apply bpow_ge_0.
-rewrite H.
+intros e; unfold ulp.
+rewrite Req_bool_true; trivial.
+case negligible_exp_spec.
+intros H1 _.
 apply generic_format_bpow.
-apply valid_exp.
-destruct (Zle_or_lt ex (fexp ex)) ; trivial.
-elim Rlt_not_le with (1 := Zx).
-rewrite Fx.
-replace (Ztrunc (scaled_mantissa beta fexp x)) with Z0.
-rewrite F2R_0.
-apply Rle_refl.
-unfold scaled_mantissa.
-rewrite canonic_exp_fexp with (1 := Ex).
-destruct (mantissa_small_pos beta fexp x ex) ; trivial.
-rewrite Ztrunc_floor.
-apply sym_eq.
-apply Zfloor_imp.
-split.
-now apply Rlt_le.
-exact H2.
-now apply Rlt_le.
-now apply Rlt_le.
+specialize (H1 (e+1)%Z); omega.
+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.
+apply Zle_trans with (1:=H4).
+replace (fexp (e+1)) with (fexp n).
+now apply le_bpow with beta.
+now apply fexp_negligible_exp_eq.
+omega.
 Qed.
 
-Theorem round_UP_succ :
-  forall x, (0 < x)%R -> F x ->
-  forall eps, (0 < eps <= ulp x)%R ->
-  round beta fexp Zceil (x + eps) = (x + ulp x)%R.
-Proof with auto with typeclass_instances.
-intros x Zx Fx eps (Heps1,[Heps2|Heps2]).
-assert (Heps: (0 <= eps < ulp x)%R).
-split.
-now apply Rlt_le.
-exact Heps2.
-assert (Hd := round_DN_succ x Zx Fx eps Heps).
-rewrite ulp_DN_UP.
-rewrite Hd.
-unfold ulp, canonic_exp.
-now rewrite ln_beta_succ.
-intros Fs.
-rewrite round_generic in Hd...
-apply Rgt_not_eq with (2 := Hd).
-pattern x at 2 ; rewrite <- Rplus_0_r.
-now apply Rplus_lt_compat_l.
-rewrite Heps2.
-apply round_generic...
-now apply generic_format_succ.
+(** The three following properties are equivalent:
+      [Exp_not_FTZ] ;  forall x, F (ulp x) ; forall x, ulp 0 <= ulp x *)
+
+Lemma generic_format_ulp: Exp_not_FTZ fexp ->
+  forall x,  F (ulp x).
+Proof.
+unfold Exp_not_FTZ; intros H x.
+case (Req_dec x 0); intros Hx.
+rewrite Hx; apply generic_format_ulp_0.
+rewrite (ulp_neq_0 _ Hx).
+apply generic_format_bpow; unfold canonic_exp.
+apply H.
 Qed.
 
-Theorem succ_le_lt:
-  forall x y,
-  F x -> F y ->
-  (0 < x < y)%R ->
-  (x + ulp x <= y)%R.
-Proof with auto with typeclass_instances.
-intros x y Hx Hy H.
-case (Rle_or_lt (ulp x) (y-x)); intros H1.
-apply Rplus_le_reg_r with (-x)%R.
-now ring_simplify (x+ulp x + -x)%R.
-replace y with (x+(y-x))%R by ring.
-absurd (x < y)%R.
-2: apply H.
-apply Rle_not_lt; apply Req_le.
-rewrite <- round_DN_succ with (eps:=(y-x)%R); try easy.
-ring_simplify (x+(y-x))%R.
-apply sym_eq.
-apply round_generic...
-split; trivial.
-apply Rlt_le; now apply Rlt_Rminus.
+Lemma not_FTZ_generic_format_ulp:
+   (forall x,  F (ulp x)) -> Exp_not_FTZ fexp.
+intros H e.
+specialize (H (bpow (e-1))).
+rewrite ulp_neq_0 in H.
+2: apply Rgt_not_eq, bpow_gt_0.
+unfold canonic_exp in H.
+rewrite ln_beta_bpow in H.
+apply generic_format_bpow_inv' in H...
+now replace (e-1+1)%Z with e in H by ring.
 Qed.
 
-(** Error of a rounding, expressed in number of ulps *)
-Theorem ulp_error :
-  forall rnd { Zrnd : Valid_rnd rnd } x,
-  (Rabs (round beta fexp rnd x - x) < ulp x)%R.
-Proof with auto with typeclass_instances.
-intros rnd Zrnd x.
-destruct (generic_format_EM beta fexp x) as [Hx|Hx].
-(* x = rnd x *)
-rewrite round_generic...
-unfold Rminus.
-rewrite Rplus_opp_r, Rabs_R0.
-apply bpow_gt_0.
-(* x <> rnd x *)
-destruct (round_DN_or_UP beta fexp rnd x) as [H|H] ; rewrite H ; clear H.
-(* . *)
-rewrite Rabs_left1.
-rewrite Ropp_minus_distr.
-apply Rplus_lt_reg_l with (round beta fexp Zfloor x).
-rewrite <- ulp_DN_UP with (1 := Hx).
-ring_simplify.
-assert (Hu: (x <= round beta fexp Zceil x)%R).
-apply round_UP_pt...
-destruct Hu as [Hu|Hu].
-exact Hu.
-elim Hx.
-rewrite Hu.
-apply generic_format_round...
-apply Rle_minus.
-apply round_DN_pt...
-(* . *)
-rewrite Rabs_pos_eq.
-rewrite ulp_DN_UP with (1 := Hx).
-apply Rplus_lt_reg_r with (x - ulp x)%R.
-ring_simplify.
-assert (Hd: (round beta fexp Zfloor x <= x)%R).
-apply round_DN_pt...
-destruct Hd as [Hd|Hd].
-exact Hd.
-elim Hx.
-rewrite <- Hd.
-apply generic_format_round...
-apply Rle_0_minus.
-apply round_UP_pt...
+
+Lemma ulp_ge_ulp_0: Exp_not_FTZ fexp ->
+  forall x,  (ulp 0 <= ulp x)%R.
+Proof.
+unfold Exp_not_FTZ; intros H x.
+case (Req_dec x 0); intros Hx.
+rewrite Hx; now right.
+unfold ulp at 1.
+rewrite Req_bool_true; trivial.
+case negligible_exp_spec'.
+intros (H1,H2); rewrite H1; apply ulp_ge_0.
+intros (n,(H1,H2)); rewrite H1.
+rewrite ulp_neq_0; trivial.
+apply bpow_le; unfold canonic_exp.
+generalize (ln_beta beta x); intros l.
+case (Zle_or_lt l (fexp l)); intros Hl.
+rewrite (fexp_negligible_exp_eq n l); trivial; apply Zle_refl.
+case (Zle_or_lt (fexp n) (fexp l)); trivial; intros K.
+absurd (fexp n <= fexp l)%Z.
+omega.
+apply Zle_trans with (2:= H _).
+apply Zeq_le, sym_eq, valid_exp; trivial.
+omega.
 Qed.
 
-Theorem ulp_half_error :
-  forall choice x,
-  (Rabs (round beta fexp (Znearest choice) x - x) <= /2 * ulp x)%R.
-Proof with auto with typeclass_instances.
-intros choice x.
-destruct (generic_format_EM beta fexp x) as [Hx|Hx].
-(* x = rnd x *)
-rewrite round_generic...
-unfold Rminus.
-rewrite Rplus_opp_r, Rabs_R0.
-apply Rmult_le_pos.
-apply Rlt_le.
-apply Rinv_0_lt_compat.
-now apply (Z2R_lt 0 2).
-apply bpow_ge_0.
-(* x <> rnd x *)
-set (d := round beta fexp Zfloor x).
-destruct (round_N_pt beta fexp choice x) as (Hr1, Hr2).
-destruct (Rle_or_lt (x - d) (d + ulp x - x)) as [H|H].
-(* . rnd(x) = rndd(x) *)
-apply Rle_trans with (Rabs (d - x)).
-apply Hr2.
-apply (round_DN_pt beta fexp x).
-rewrite Rabs_left1.
-rewrite Ropp_minus_distr.
-apply Rmult_le_reg_r with 2%R.
-now apply (Z2R_lt 0 2).
-apply Rplus_le_reg_r with (d - x)%R.
-ring_simplify.
-apply Rle_trans with (1 := H).
-right. field.
-apply Rle_minus.
-apply (round_DN_pt beta fexp x).
-(* . rnd(x) = rndu(x) *)
-assert (Hu: (d + ulp x)%R = round beta fexp Zceil x).
-unfold d.
-now rewrite <- ulp_DN_UP.
-apply Rle_trans with (Rabs (d + ulp x - x)).
-apply Hr2.
-rewrite Hu.
-apply (round_UP_pt beta fexp x).
-rewrite Rabs_pos_eq.
-apply Rmult_le_reg_r with 2%R.
-now apply (Z2R_lt 0 2).
-apply Rplus_le_reg_r with (- (d + ulp x - x))%R.
-ring_simplify.
-apply Rlt_le.
-apply Rlt_le_trans with (1 := H).
-right. field.
-apply Rle_0_minus.
-rewrite Hu.
-apply (round_UP_pt beta fexp x).
+Lemma not_FTZ_ulp_ge_ulp_0:
+   (forall x,  (ulp 0 <= ulp x)%R) -> Exp_not_FTZ fexp.
+Proof.
+intros H e.
+apply generic_format_bpow_inv' with beta.
+apply generic_format_bpow_ge_ulp_0.
+replace e with ((e-1)+1)%Z by ring.
+rewrite <- ulp_bpow.
+apply H.
 Qed.
 
-Theorem ulp_le :
+
+
+Theorem ulp_le_pos :
   forall { Hm : Monotone_exp fexp },
   forall x y: R,
-  (0 < x)%R -> (x <= y)%R ->
+  (0 <= x)%R -> (x <= y)%R ->
   (ulp x <= ulp y)%R.
-Proof.
+Proof with auto with typeclass_instances.
 intros Hm x y Hx Hxy.
+destruct Hx as [Hx|Hx].
+rewrite ulp_neq_0.
+rewrite ulp_neq_0.
 apply bpow_le.
 apply Hm.
 now apply ln_beta_le.
+apply Rgt_not_eq, Rlt_gt.
+now apply Rlt_le_trans with (1:=Hx).
+now apply Rgt_not_eq.
+rewrite <- Hx.
+apply ulp_ge_ulp_0.
+apply monotone_exp_not_FTZ...
 Qed.
 
-Theorem ulp_bpow :
-  forall e, ulp (bpow e) = bpow (fexp (e + 1)).
-intros e.
-unfold ulp.
-apply f_equal.
-apply canonic_exp_fexp.
-rewrite Rabs_pos_eq.
-split.
-ring_simplify (e + 1 - 1)%Z.
-apply Rle_refl.
-apply bpow_lt.
-apply Zlt_succ.
-apply bpow_ge_0.
-Qed.
 
-Theorem ulp_DN :
-  forall x,
-  (0 < round beta fexp Zfloor x)%R ->
-  ulp (round beta fexp Zfloor x) = ulp x.
+Theorem ulp_le :
+  forall { Hm : Monotone_exp fexp },
+  forall x y: R,
+  (Rabs x <= Rabs y)%R ->
+  (ulp x <= ulp y)%R.
 Proof.
-intros x Hd.
-unfold ulp.
-now rewrite canonic_exp_DN with (2 := Hd).
+intros Hm x y Hxy.
+rewrite <- ulp_abs.
+rewrite <- (ulp_abs y).
+apply ulp_le_pos; trivial.
+apply Rabs_pos.
 Qed.
 
-Theorem ulp_error_f :
-  forall { Hm : Monotone_exp fexp } rnd { Zrnd : Valid_rnd rnd } x,
-  (round beta fexp rnd x <> 0)%R ->
-  (Rabs (round beta fexp rnd x - x) < ulp (round beta fexp rnd x))%R.
-Proof with auto with typeclass_instances.
-intros Hm rnd Zrnd x Hfx.
-case (round_DN_or_UP beta fexp rnd x); intros Hx.
-(* *)
-case (Rle_or_lt 0 (round beta fexp Zfloor x)).
-intros H; destruct H.
-rewrite Hx at 2.
-rewrite ulp_DN; trivial.
-apply ulp_error...
-rewrite Hx in Hfx; contradict Hfx; auto with real.
-intros H.
-apply Rlt_le_trans with (1:=ulp_error _ _).
-rewrite <- (ulp_opp x), <- (ulp_opp (round beta fexp rnd x)).
-apply ulp_le; trivial.
-apply Ropp_0_gt_lt_contravar; apply Rlt_gt.
-case (Rle_or_lt 0 x); trivial.
-intros H1; contradict H.
-apply Rle_not_lt.
-apply round_ge_generic...
-apply generic_format_0.
-apply Ropp_le_contravar; rewrite Hx.
-apply (round_DN_pt beta fexp x).
-(* *)
-rewrite Hx; case (Rle_or_lt 0 (round beta fexp Zceil x)).
-intros H; destruct H.
-apply Rlt_le_trans with (1:=ulp_error _ _).
-apply ulp_le; trivial.
-case (Rle_or_lt x 0); trivial.
-intros H1; contradict H.
-apply Rle_not_lt.
-apply round_le_generic...
-apply generic_format_0.
-apply round_UP_pt...
-rewrite Hx in Hfx; contradict Hfx; auto with real.
-intros H.
-rewrite <- (ulp_opp (round beta fexp Zceil x)).
-rewrite <- round_DN_opp.
-rewrite ulp_DN; trivial.
-replace (round beta fexp Zceil x - x)%R with (-((round beta fexp Zfloor (-x) - (-x))))%R.
-rewrite Rabs_Ropp.
-apply ulp_error...
-rewrite round_DN_opp; ring.
-rewrite round_DN_opp; apply Ropp_0_gt_lt_contravar; apply Rlt_gt; assumption.
-Qed.
 
-Theorem ulp_half_error_f :
-  forall { Hm : Monotone_exp fexp },
-  forall choice x,
-  (round beta fexp (Znearest choice) x <> 0)%R ->
-  (Rabs (round beta fexp (Znearest choice) x - x) <= /2 * ulp (round beta fexp (Znearest choice) x))%R.
-Proof with auto with typeclass_instances.
-intros Hm choice x Hfx.
-case (round_DN_or_UP beta fexp (Znearest choice) x); intros Hx.
-(* *)
-case (Rle_or_lt 0 (round beta fexp Zfloor x)).
-intros H; destruct H.
-rewrite Hx at 2.
-rewrite ulp_DN; trivial.
-apply ulp_half_error.
-rewrite Hx in Hfx; contradict Hfx; auto with real.
-intros H.
-apply Rle_trans with (1:=ulp_half_error _ _).
-apply Rmult_le_compat_l.
-auto with real.
-rewrite <- (ulp_opp x), <- (ulp_opp (round beta fexp (Znearest choice) x)).
-apply ulp_le; trivial.
-apply Ropp_0_gt_lt_contravar; apply Rlt_gt.
-case (Rle_or_lt 0 x); trivial.
-intros H1; contradict H.
-apply Rle_not_lt.
-apply round_ge_generic...
-apply generic_format_0.
-apply Ropp_le_contravar; rewrite Hx.
-apply (round_DN_pt beta fexp x).
-(* *)
-case (Rle_or_lt 0 (round beta fexp Zceil x)).
-intros H; destruct H.
-apply Rle_trans with (1:=ulp_half_error _ _).
-apply Rmult_le_compat_l.
-auto with real.
-apply ulp_le; trivial.
-case (Rle_or_lt x 0); trivial.
-intros H1; contradict H.
-apply Rle_not_lt.
-apply round_le_generic...
-apply generic_format_0.
-rewrite Hx; apply (round_UP_pt beta fexp x).
-rewrite Hx in Hfx; contradict Hfx; auto with real.
-intros H.
-rewrite Hx at 2; rewrite <- (ulp_opp (round beta fexp Zceil x)).
-rewrite <- round_DN_opp.
-rewrite ulp_DN; trivial.
-pattern x at 1 2; rewrite <- Ropp_involutive.
-rewrite round_N_opp.
-unfold Rminus.
-rewrite <- Ropp_plus_distr, Rabs_Ropp.
-apply ulp_half_error.
-rewrite round_DN_opp; apply Ropp_0_gt_lt_contravar; apply Rlt_gt; assumption.
-Qed.
 
-(** Predecessor *)
-Definition pred x :=
+(** Definition and properties of pred and succ *)
+
+Definition pred_pos x :=
   if Req_bool x (bpow (ln_beta beta x - 1)) then
     (x - bpow (fexp (ln_beta beta x - 1)))%R
   else
     (x - ulp x)%R.
 
-Theorem pred_ge_bpow :
+Definition succ x :=
+   if (Rle_bool 0 x) then
+          (x+ulp x)%R
+   else
+     (- pred_pos (-x))%R.
+
+Definition pred x := (- succ (-x))%R.
+
+Theorem pred_eq_pos:
+  forall x, (0 <= x)%R -> (pred x = pred_pos x)%R.
+Proof.
+intros x Hx; unfold pred, succ.
+case Rle_bool_spec; intros Hx'.
+assert (K:(x = 0)%R).
+apply Rle_antisym; try assumption.
+apply Ropp_le_cancel.
+now rewrite Ropp_0.
+rewrite K; unfold pred_pos.
+rewrite Req_bool_false.
+2: apply Rlt_not_eq, bpow_gt_0.
+rewrite Ropp_0; ring.
+now rewrite 2!Ropp_involutive.
+Qed.
+
+Theorem succ_eq_pos:
+  forall x, (0 <= x)%R -> (succ x = x + ulp x)%R.
+Proof.
+intros x Hx; unfold succ.
+now rewrite Rle_bool_true.
+Qed.
+
+Lemma pred_eq_opp_succ_opp: forall x, pred x = (- succ (-x))%R.
+Proof.
+reflexivity.
+Qed.
+
+Lemma succ_eq_opp_pred_opp: forall x, succ x = (- pred (-x))%R.
+Proof.
+intros x; unfold pred.
+now rewrite 2!Ropp_involutive.
+Qed.
+
+Lemma succ_opp: forall x, (succ (-x) = - pred x)%R.
+Proof.
+intros x; rewrite succ_eq_opp_pred_opp.
+now rewrite Ropp_involutive.
+Qed.
+
+Lemma pred_opp: forall x, (pred (-x) = - succ x)%R.
+Proof.
+intros x; rewrite pred_eq_opp_succ_opp.
+now rewrite Ropp_involutive.
+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 *)
+(* was pred_ge_bpow *)
+Theorem id_m_ulp_ge_bpow :
   forall x e,  F x ->
   x <> ulp x ->
   (bpow e < x)%R ->
@@ -573,7 +442,8 @@ omega.
 case (Zle_lt_or_eq _ _ H); intros Hm.
 (* *)
 pattern x at 1 ; rewrite Fx.
-unfold ulp, F2R. simpl.
+rewrite ulp_neq_0.
+unfold F2R. simpl.
 pattern (bpow (canonic_exp beta fexp x)) at 2 ; rewrite <- Rmult_1_l.
 rewrite <- Rmult_minus_distr_r.
 change 1%R with (Z2R 1).
@@ -581,15 +451,44 @@ rewrite <- Z2R_minus.
 change (bpow e <= F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x) - 1) (canonic_exp beta fexp x)))%R.
 apply bpow_le_F2R_m1; trivial.
 now rewrite <- Fx.
+apply Rgt_not_eq, Rlt_gt.
+apply Rlt_trans with (2:=Hx), bpow_gt_0.
 (* *)
 contradict Hx'.
 pattern x at 1; rewrite Fx.
 rewrite  <- Hm.
-unfold ulp, F2R; simpl.
+rewrite ulp_neq_0.
+unfold F2R; simpl.
 now rewrite Rmult_1_l.
+apply Rgt_not_eq, Rlt_gt.
+apply Rlt_trans with (2:=Hx), bpow_gt_0.
 Qed.
 
-Lemma generic_format_pred_1:
+(* was succ_le_bpow *)
+Theorem id_p_ulp_le_bpow :
+  forall x e, (0 < x)%R -> F x ->
+  (x < bpow e)%R ->
+  (x + ulp x <= bpow e)%R.
+Proof.
+intros x e Zx Fx Hx.
+pattern x at 1 ; rewrite Fx.
+rewrite ulp_neq_0.
+unfold F2R. simpl.
+pattern (bpow (canonic_exp beta fexp x)) at 2 ; rewrite <- Rmult_1_l.
+rewrite <- Rmult_plus_distr_r.
+change 1%R with (Z2R 1).
+rewrite <- Z2R_plus.
+change (F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x) + 1) (canonic_exp beta fexp x)) <= bpow e)%R.
+apply F2R_p1_le_bpow.
+apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
+now rewrite <- Fx.
+now rewrite <- Fx.
+now apply Rgt_not_eq.
+Qed.
+
+
+
+Lemma generic_format_pred_aux1:
   forall x, (0 < x)%R -> F x ->
   x <> bpow (ln_beta beta x - 1) ->
   F (x - ulp x).
@@ -606,7 +505,8 @@ now apply Rlt_le.
 unfold generic_format, scaled_mantissa, canonic_exp.
 rewrite ln_beta_unique with beta (x - ulp x)%R ex.
 pattern x at 1 3 ; rewrite Fx.
-unfold ulp, scaled_mantissa.
+rewrite ulp_neq_0.
+unfold scaled_mantissa.
 rewrite canonic_exp_fexp with (1 := Ex).
 unfold F2R. simpl.
 rewrite Rmult_minus_distr_r.
@@ -618,23 +518,27 @@ rewrite Ztrunc_Z2R.
 rewrite Z2R_minus.
 rewrite Rmult_minus_distr_r.
 now rewrite Rmult_1_l.
+now apply Rgt_not_eq.
 rewrite Rabs_pos_eq.
 split.
-apply pred_ge_bpow; trivial.
-unfold ulp; intro H.
+apply id_m_ulp_ge_bpow; trivial.
+rewrite ulp_neq_0.
+intro H.
 assert (ex-1 < canonic_exp beta fexp x  < ex)%Z.
 split ; apply (lt_bpow beta) ; rewrite <- H ; easy.
 clear -H0. omega.
+now apply Rgt_not_eq.
 apply Ex'.
 apply Rle_lt_trans with (2 := proj2 Ex').
 pattern x at 3 ; rewrite <- Rplus_0_r.
 apply Rplus_le_compat_l.
 rewrite <-Ropp_0.
 apply Ropp_le_contravar.
-apply bpow_ge_0.
+apply ulp_ge_0.
 apply Rle_0_minus.
 pattern x at 2; rewrite Fx.
-unfold ulp, F2R; simpl.
+rewrite ulp_neq_0.
+unfold F2R; simpl.
 pattern (bpow (canonic_exp beta fexp x)) at 1; rewrite <- Rmult_1_l.
 apply Rmult_le_compat_r.
 apply bpow_ge_0.
@@ -646,9 +550,10 @@ rewrite <- Fx.
 apply Rle_lt_trans with (2:=proj1 Ex').
 apply bpow_ge_0.
 omega.
+now apply Rgt_not_eq.
 Qed.
 
-Lemma generic_format_pred_2 :
+Lemma generic_format_pred_aux2 :
   forall x, (0 < x)%R -> F x ->
   let e := ln_beta_val beta x (ln_beta beta x) in
   x =  bpow (e - 1) ->
@@ -712,109 +617,210 @@ rewrite Hx, He.
 ring.
 Qed.
 
-Theorem generic_format_pred :
+
+Theorem generic_format_succ_aux1 :
   forall x, (0 < x)%R -> F x ->
-  F (pred x).
+  F (x + ulp x).
 Proof.
 intros x Zx Fx.
+destruct (ln_beta beta x) as (ex, Ex).
+specialize (Ex (Rgt_not_eq _ _ Zx)).
+assert (Ex' := Ex).
+rewrite Rabs_pos_eq in Ex'.
+destruct (id_p_ulp_le_bpow x ex) ; try easy.
+unfold generic_format, scaled_mantissa, canonic_exp.
+rewrite ln_beta_unique with beta (x + ulp x)%R ex.
+pattern x at 1 3 ; rewrite Fx.
+rewrite ulp_neq_0.
+unfold scaled_mantissa.
+rewrite canonic_exp_fexp with (1 := Ex).
+unfold F2R. simpl.
+rewrite Rmult_plus_distr_r.
+rewrite Rmult_assoc.
+rewrite <- bpow_plus, Zplus_opp_r, Rmult_1_r.
+change (bpow 0) with (Z2R 1).
+rewrite <- Z2R_plus.
+rewrite Ztrunc_Z2R.
+rewrite Z2R_plus.
+rewrite Rmult_plus_distr_r.
+now rewrite Rmult_1_l.
+now apply Rgt_not_eq.
+rewrite Rabs_pos_eq.
+split.
+apply Rle_trans with (1 := proj1 Ex').
+pattern x at 1 ; rewrite <- Rplus_0_r.
+apply Rplus_le_compat_l.
+apply ulp_ge_0.
+exact H.
+apply Rplus_le_le_0_compat.
+now apply Rlt_le.
+apply ulp_ge_0.
+rewrite H.
+apply generic_format_bpow.
+apply valid_exp.
+destruct (Zle_or_lt ex (fexp ex)) ; trivial.
+elim Rlt_not_le with (1 := Zx).
+rewrite Fx.
+replace (Ztrunc (scaled_mantissa beta fexp x)) with Z0.
+rewrite F2R_0.
+apply Rle_refl.
+unfold scaled_mantissa.
+rewrite canonic_exp_fexp with (1 := Ex).
+destruct (mantissa_small_pos beta fexp x ex) ; trivial.
+rewrite Ztrunc_floor.
+apply sym_eq.
+apply Zfloor_imp.
+split.
+now apply Rlt_le.
+exact H2.
+now apply Rlt_le.
+now apply Rlt_le.
+Qed.
+
+Theorem generic_format_pred_pos :
+  forall x, F x -> (0 < x)%R ->
+  F (pred_pos x).
+Proof.
+intros x Fx Zx.
+unfold pred_pos; case Req_bool_spec; intros H.
+now apply generic_format_pred_aux2.
+now apply generic_format_pred_aux1.
+Qed.
+
+
+Theorem generic_format_succ :
+  forall x, F x ->
+  F (succ x).
+Proof.
+intros x Fx.
+unfold succ; case Rle_bool_spec; intros Zx.
+destruct Zx as [Zx|Zx].
+now apply generic_format_succ_aux1.
+rewrite <- Zx, Rplus_0_l.
+apply generic_format_ulp_0.
+apply generic_format_opp.
+apply generic_format_pred_pos.
+now apply generic_format_opp.
+now apply Ropp_0_gt_lt_contravar.
+Qed.
+
+Theorem generic_format_pred :
+  forall x, F x ->
+  F (pred x).
+Proof.
+intros x Fx.
 unfold pred.
-case Req_bool_spec; intros H.
-now apply generic_format_pred_2.
-now apply generic_format_pred_1.
+apply generic_format_opp.
+apply generic_format_succ.
+now apply generic_format_opp.
 Qed.
 
-Theorem generic_format_plus_ulp :
-  forall { monotone_exp : Monotone_exp fexp },
+
+
+Theorem pred_pos_lt_id :
   forall x, (x <> 0)%R ->
-  F x -> F (x + ulp x).
-Proof with auto with typeclass_instances.
-intros monotone_exp x Zx Fx.
-destruct (Rtotal_order x 0) as [Hx|[Hx|Hx]].
-rewrite <- Ropp_involutive.
-apply generic_format_opp.
-rewrite Ropp_plus_distr, <- ulp_opp.
-apply generic_format_opp in Fx.
-destruct (Req_dec (-x) (bpow (ln_beta beta (-x) - 1))) as [Hx'|Hx'].
-rewrite Hx' in Fx |- *.
-apply generic_format_bpow_inv' in Fx...
-unfold ulp, canonic_exp.
-rewrite ln_beta_bpow.
-revert Fx.
-generalize (ln_beta_val _ _ (ln_beta beta (-x)) - 1)%Z.
-clear -monotone_exp valid_exp.
-intros e He.
-destruct (Zle_lt_or_eq _ _ He) as [He1|He1].
-assert (He2 : e = (e - fexp (e + 1) + fexp (e + 1))%Z) by ring.
-rewrite He2 at 1.
-rewrite bpow_plus.
-assert (Hb := Z2R_Zpower beta _ (Zle_minus_le_0 _ _ He)).
-match goal with |- F (?a * ?b + - ?b) =>
-  replace (a * b + -b)%R with ((a - 1) * b)%R by ring end.
-rewrite <- Hb.
-rewrite <- (Z2R_minus _ 1).
-change (F (F2R (Float beta (Zpower beta (e - fexp (e + 1)) - 1) (fexp (e + 1))))).
-apply generic_format_F2R.
-intros Zb.
-unfold canonic_exp.
-rewrite ln_beta_F2R with (1 := Zb).
-rewrite (ln_beta_unique beta _ (e - fexp (e + 1))).
-apply monotone_exp.
-rewrite <- He2.
-apply Zle_succ.
-rewrite Rabs_pos_eq.
-rewrite Z2R_minus, Hb.
-split.
-apply Rplus_le_reg_r with (- bpow (e - fexp (e + 1) - 1) + Z2R 1)%R.
-apply Rmult_le_reg_r with (bpow (-(e - fexp (e+1) - 1))).
+  (pred_pos x < x)%R.
+Proof.
+intros x Zx.
+unfold pred_pos.
+case Req_bool_spec; intros H.
+(* *)
+rewrite <- Rplus_0_r.
+apply Rplus_lt_compat_l.
+rewrite <- Ropp_0.
+apply Ropp_lt_contravar.
 apply bpow_gt_0.
-ring_simplify.
-apply Rle_trans with R1.
-rewrite Rmult_1_l.
-apply (bpow_le _ _ 0).
-clear -He1 ; omega.
-rewrite Ropp_mult_distr_l_reverse.
-rewrite <- 2!bpow_plus.
-ring_simplify (e - fexp (e + 1) - 1 + - (e - fexp (e + 1) - 1))%Z.
-ring_simplify (- (e - fexp (e + 1) - 1) + (e - fexp (e + 1)))%Z.
-rewrite bpow_1.
-rewrite <- (Z2R_plus (-1) _).
-apply (Z2R_le 1).
-generalize (Zle_bool_imp_le _ _ (radix_prop beta)).
-clear ; omega.
-rewrite <- (Rplus_0_r (bpow (e - fexp (e + 1)))) at 2.
+(* *)
+rewrite <- Rplus_0_r.
 apply Rplus_lt_compat_l.
-now apply (Z2R_lt (-1) 0).
-rewrite Z2R_minus.
-apply Rle_0_minus.
-rewrite Hb.
-apply (bpow_le _ 0).
-now apply Zle_minus_le_0.
-rewrite He1, Rplus_opp_r.
-apply generic_format_0.
-apply generic_format_pred_1 ; try easy.
 rewrite <- Ropp_0.
-now apply Ropp_lt_contravar.
-now elim Zx.
-now apply generic_format_succ.
+apply Ropp_lt_contravar.
+rewrite ulp_neq_0; trivial.
+apply bpow_gt_0.
 Qed.
 
-Theorem generic_format_minus_ulp :
-  forall { monotone_exp : Monotone_exp fexp },
+Theorem succ_gt_id :
   forall x, (x <> 0)%R ->
-  F x -> F (x - ulp x).
+  (x < succ x)%R.
 Proof.
-intros monotone_exp x Zx Fx.
-replace (x - ulp x)%R with (-(-x + ulp x))%R by ring.
-apply generic_format_opp.
-rewrite <- ulp_opp.
-apply generic_format_plus_ulp.
-contradict Zx.
-rewrite <- (Ropp_involutive x), Zx.
-apply Ropp_0.
-now apply generic_format_opp.
+intros x Zx; unfold succ.
+case Rle_bool_spec; intros Hx.
+pattern x at 1; rewrite <- (Rplus_0_r x).
+apply Rplus_lt_compat_l.
+rewrite ulp_neq_0; trivial.
+apply bpow_gt_0.
+pattern x at 1; rewrite <- (Ropp_involutive x).
+apply Ropp_lt_contravar.
+apply pred_pos_lt_id.
+now auto with real.
 Qed.
 
-Lemma pred_plus_ulp_1 :
+
+Theorem pred_lt_id :
+  forall x,  (x <> 0)%R ->
+  (pred x < x)%R.
+Proof.
+intros x Zx; unfold pred.
+pattern x at 2; rewrite <- (Ropp_involutive x).
+apply Ropp_lt_contravar.
+apply succ_gt_id.
+now auto with real.
+Qed.
+
+Theorem succ_ge_id :
+  forall x, (x <= succ x)%R.
+Proof.
+intros x; case (Req_dec x 0).
+intros V; rewrite V.
+unfold succ; rewrite Rle_bool_true;[idtac|now right].
+rewrite Rplus_0_l; apply ulp_ge_0.
+intros; left; now apply succ_gt_id.
+Qed.
+
+
+Theorem pred_le_id :
+  forall x,  (pred x <= x)%R.
+Proof.
+intros x; unfold pred.
+pattern x at 2; rewrite <- (Ropp_involutive x).
+apply Ropp_le_contravar.
+apply succ_ge_id.
+Qed.
+
+
+Theorem pred_pos_ge_0 :
+  forall x,
+  (0 < x)%R -> F x -> (0 <= pred_pos x)%R.
+Proof.
+intros x Zx Fx.
+unfold pred_pos.
+case Req_bool_spec; intros H.
+(* *)
+apply Rle_0_minus.
+rewrite H.
+apply bpow_le.
+destruct (ln_beta beta x) as (ex,Ex) ; simpl.
+rewrite ln_beta_bpow.
+ring_simplify (ex - 1 + 1 - 1)%Z.
+apply generic_format_bpow_inv with beta; trivial.
+simpl in H.
+rewrite <- H; assumption.
+apply Rle_0_minus.
+now apply ulp_le_id.
+Qed.
+
+Theorem pred_ge_0 :
+  forall x,
+  (0 < x)%R -> F x -> (0 <= pred x)%R.
+Proof.
+intros x Zx Fx.
+rewrite pred_eq_pos.
+now apply pred_pos_ge_0.
+now left.
+Qed.
+
+
+Lemma pred_pos_plus_ulp_aux1 :
   forall x, (0 < x)%R -> F x ->
   x <> bpow (ln_beta beta x - 1) ->
   ((x - ulp x) + ulp (x-ulp x) = x)%R.
@@ -822,24 +828,40 @@ Proof.
 intros x Zx Fx Hx.
 replace (ulp (x - ulp x)) with (ulp x).
 ring.
-unfold ulp at 1 2; apply f_equal.
+assert (H:(x <> 0)%R) by auto with real.
+assert (H':(x <> bpow (canonic_exp beta fexp x))%R).
+unfold canonic_exp; intros M.
+case_eq (ln_beta beta x); intros ex Hex T.
+assert (Lex:(ln_beta_val beta x (ln_beta beta x) = ex)%Z).
+rewrite T; reflexivity.
+rewrite Lex in *.
+clear T; simpl in *; specialize (Hex H).
+rewrite Rabs_right in Hex.
+2: apply Rle_ge; apply Rlt_le; easy.
+assert (ex-1 < fexp ex  < ex)%Z.
+split ; apply (lt_bpow beta); rewrite <- M;[idtac|easy].
+destruct (proj1 Hex);[trivial|idtac].
+contradict Hx; auto with real.
+omega.
+rewrite 2!ulp_neq_0; try auto with real.
+apply f_equal.
 unfold canonic_exp; apply f_equal.
-destruct (ln_beta beta x) as (ex, Hex).
-simpl in *.
-assert (x <> 0)%R by auto with real.
+case_eq (ln_beta beta x); intros ex Hex T.
+assert (Lex:(ln_beta_val beta x (ln_beta beta x) = ex)%Z).
+rewrite T; reflexivity.
+rewrite Lex in *; simpl in *; clear T.
 specialize (Hex H).
-apply sym_eq.
-apply ln_beta_unique.
+apply sym_eq, ln_beta_unique.
 rewrite Rabs_right.
 rewrite Rabs_right in Hex.
 2: apply Rle_ge; apply Rlt_le; easy.
 split.
 destruct Hex as ([H1|H1],H2).
-apply pred_ge_bpow; trivial.
-unfold ulp; intros H3.
-assert (ex-1 < canonic_exp beta fexp x  < ex)%Z.
-split ; apply (lt_bpow beta) ; rewrite <- H3 ; easy.
-omega.
+apply Rle_trans with (x-ulp x)%R.
+apply id_m_ulp_ge_bpow; trivial.
+rewrite ulp_neq_0; trivial.
+rewrite ulp_neq_0; trivial.
+right; unfold canonic_exp; now rewrite Lex.
 contradict Hx; auto with real.
 apply Rle_lt_trans with (2:=proj2 Hex).
 rewrite <- Rplus_0_r.
@@ -849,9 +871,10 @@ apply Ropp_le_contravar.
 apply bpow_ge_0.
 apply Rle_ge.
 apply Rle_0_minus.
-pattern x at 2; rewrite Fx.
-unfold ulp, F2R; simpl.
-pattern (bpow (canonic_exp beta fexp x)) at 1; rewrite <- Rmult_1_l.
+rewrite Fx.
+unfold F2R, canonic_exp; simpl.
+rewrite Lex.
+pattern (bpow (fexp ex)) at 1; rewrite <- Rmult_1_l.
 apply Rmult_le_compat_r.
 apply bpow_ge_0.
 replace 1%R with (Z2R (Zsucc 0)) by reflexivity.
@@ -861,7 +884,8 @@ apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
 now rewrite <- Fx.
 Qed.
 
-Lemma pred_plus_ulp_2 :
+
+Lemma pred_pos_plus_ulp_aux2 :
   forall x, (0 < x)%R -> F x ->
   let e := ln_beta_val beta x (ln_beta beta x) in
   x =  bpow (e - 1) ->
@@ -876,7 +900,8 @@ apply generic_format_bpow_inv with beta; trivial.
 rewrite <- Hxe; assumption.
 case (Zle_lt_or_eq _ _ He); clear He; intros He.
 (* *)
-unfold ulp; apply f_equal.
+rewrite ulp_neq_0; trivial.
+apply f_equal.
 unfold canonic_exp; apply f_equal.
 apply sym_eq.
 apply ln_beta_unique.
@@ -915,90 +940,271 @@ contradict Zp.
 rewrite Hxe, He; ring.
 Qed.
 
-Theorem pred_plus_ulp :
+Lemma pred_pos_plus_ulp_aux3 :
   forall x, (0 < x)%R -> F x ->
-  (pred x <> 0)%R ->
-  (pred x + ulp (pred x) = x)%R.
+  let e := ln_beta_val beta x (ln_beta beta x) in
+  x =  bpow (e - 1) ->
+  (x - bpow (fexp (e-1)) = 0)%R ->
+  (ulp 0 = x)%R.
 Proof.
-intros x Zx Fx.
-unfold pred.
-case Req_bool_spec; intros H Zp.
-now apply pred_plus_ulp_2.
-now apply pred_plus_ulp_1.
+intros x Hx Fx e H1 H2.
+assert (H3:(x = bpow (fexp (e - 1)))).
+now apply Rminus_diag_uniq.
+assert (H4: (fexp (e-1) = e-1)%Z).
+apply bpow_inj with beta.
+now rewrite <- H1.
+unfold ulp; rewrite Req_bool_true; trivial.
+case negligible_exp_spec.
+intros K.
+specialize (K (e-1)%Z).
+contradict K; omega.
+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.
 Qed.
 
-Theorem pred_lt_id :
-  forall x,
-  (pred x < x)%R.
+
+
+
+(** The following one is false for x = 0 in FTZ *)
+
+Theorem pred_pos_plus_ulp :
+  forall x, (0 < x)%R -> F x ->
+  (pred_pos x + ulp (pred_pos x) = x)%R.
 Proof.
-intros.
-unfold pred.
+intros x Zx Fx.
+unfold pred_pos.
 case Req_bool_spec; intros H.
-(* *)
-rewrite <- Rplus_0_r.
-apply Rplus_lt_compat_l.
-rewrite <- Ropp_0.
-apply Ropp_lt_contravar.
+case (Req_EM_T (x - bpow (fexp (ln_beta_val beta x (ln_beta beta x) -1))) 0); intros H1.
+rewrite H1, Rplus_0_l.
+now apply pred_pos_plus_ulp_aux3.
+now apply pred_pos_plus_ulp_aux2.
+now apply pred_pos_plus_ulp_aux1.
+Qed.
+
+
+
+
+(** Rounding x + small epsilon *)
+
+Theorem ln_beta_plus_eps:
+  forall x, (0 < x)%R -> F x ->
+  forall eps, (0 <= eps < ulp x)%R ->
+  ln_beta beta (x + eps) = ln_beta beta x :> Z.
+Proof.
+intros x Zx Fx eps Heps.
+destruct (ln_beta beta x) as (ex, He).
+simpl.
+specialize (He (Rgt_not_eq _ _ Zx)).
+apply ln_beta_unique.
+rewrite Rabs_pos_eq.
+rewrite Rabs_pos_eq in He.
+split.
+apply Rle_trans with (1 := proj1 He).
+pattern x at 1 ; rewrite <- Rplus_0_r.
+now apply Rplus_le_compat_l.
+apply Rlt_le_trans with (x + ulp x)%R.
+now apply Rplus_lt_compat_l.
+pattern x at 1 ; rewrite Fx.
+rewrite ulp_neq_0.
+unfold F2R. simpl.
+pattern (bpow (canonic_exp beta fexp x)) at 2 ; rewrite <- Rmult_1_l.
+rewrite <- Rmult_plus_distr_r.
+change 1%R with (Z2R 1).
+rewrite <- Z2R_plus.
+change (F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x) + 1) (canonic_exp beta fexp x)) <= bpow ex)%R.
+apply F2R_p1_le_bpow.
+apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
+now rewrite <- Fx.
+now rewrite <- Fx.
+now apply Rgt_not_eq.
+now apply Rlt_le.
+apply Rplus_le_le_0_compat.
+now apply Rlt_le.
+apply Heps.
+Qed.
+
+Theorem round_DN_plus_eps_pos:
+  forall x, (0 <= x)%R -> F x ->
+  forall eps, (0 <= eps < ulp x)%R ->
+  round beta fexp Zfloor (x + eps) = x.
+Proof.
+intros x Zx Fx eps Heps.
+destruct Zx as [Zx|Zx].
+(* . 0 < x *)
+pattern x at 2 ; rewrite Fx.
+unfold round.
+unfold scaled_mantissa. simpl.
+unfold canonic_exp at 1 2.
+rewrite ln_beta_plus_eps ; trivial.
+apply (f_equal (fun m => F2R (Float beta m _))).
+rewrite Ztrunc_floor.
+apply Zfloor_imp.
+split.
+apply (Rle_trans _ _ _ (Zfloor_lb _)).
+apply Rmult_le_compat_r.
+apply bpow_ge_0.
+pattern x at 1 ; rewrite <- Rplus_0_r.
+now apply Rplus_le_compat_l.
+apply Rlt_le_trans with ((x + ulp x) * bpow (- canonic_exp beta fexp x))%R.
+apply Rmult_lt_compat_r.
 apply bpow_gt_0.
-(* *)
-rewrite <- Rplus_0_r.
-apply Rplus_lt_compat_l.
-rewrite <- Ropp_0.
-apply Ropp_lt_contravar.
+now apply Rplus_lt_compat_l.
+rewrite Rmult_plus_distr_r.
+rewrite Z2R_plus.
+apply Rplus_le_compat.
+pattern x at 1 3 ; rewrite Fx.
+unfold F2R. simpl.
+rewrite Rmult_assoc.
+rewrite <- bpow_plus.
+rewrite Zplus_opp_r.
+rewrite Rmult_1_r.
+rewrite Zfloor_Z2R.
+apply Rle_refl.
+rewrite ulp_neq_0.
+2: now apply Rgt_not_eq.
+rewrite <- bpow_plus.
+rewrite Zplus_opp_r.
+apply Rle_refl.
+apply Rmult_le_pos.
+now apply Rlt_le.
+apply bpow_ge_0.
+(* . x=0 *)
+rewrite <- Zx, Rplus_0_l; rewrite <- Zx in Heps.
+case (proj1 Heps); intros P.
+unfold round, scaled_mantissa, canonic_exp.
+revert Heps; unfold ulp.
+rewrite Req_bool_true; trivial.
+case negligible_exp_spec.
+intros _ (H1,H2).
+absurd (0 < 0)%R; auto with real.
+now apply Rle_lt_trans with (1:=H1).
+intros n Hn H.
+assert (fexp (ln_beta beta eps) = fexp n).
+apply valid_exp; try assumption.
+assert(ln_beta beta eps-1 < fexp n)%Z;[idtac|omega].
+apply lt_bpow with beta.
+apply Rle_lt_trans with (2:=proj2 H).
+destruct (ln_beta beta eps) as (e,He).
+simpl; rewrite Rabs_pos_eq in He.
+now apply He, Rgt_not_eq.
+now left.
+replace (Zfloor (eps * bpow (- fexp (ln_beta beta eps)))) with 0%Z.
+unfold F2R; simpl; ring.
+apply sym_eq, Zfloor_imp.
+split.
+apply Rmult_le_pos.
+now left.
+apply bpow_ge_0.
+apply Rmult_lt_reg_r with (bpow (fexp n)).
 apply bpow_gt_0.
+rewrite Rmult_assoc, <- bpow_plus.
+rewrite H0; ring_simplify (-fexp n + fexp n)%Z.
+simpl; rewrite Rmult_1_l, Rmult_1_r.
+apply H.
+rewrite <- P, round_0; trivial.
+apply valid_rnd_DN.
 Qed.
 
-Theorem pred_ge_0 :
-  forall x,
-  (0 < x)%R -> F x -> (0 <= pred x)%R.
-intros x Zx Fx.
-unfold pred.
-case Req_bool_spec; intros H.
-(* *)
-apply Rle_0_minus.
-rewrite H.
-apply bpow_le.
-destruct (ln_beta beta x) as (ex,Ex) ; simpl.
-rewrite ln_beta_bpow.
-ring_simplify (ex - 1 + 1 - 1)%Z.
-apply generic_format_bpow_inv with beta; trivial.
-simpl in H.
-rewrite <- H; assumption.
-apply Rle_0_minus.
-now apply ulp_le_id.
+
+Theorem round_UP_plus_eps_pos :
+  forall x, (0 <= x)%R -> F x ->
+  forall eps, (0 < eps <= ulp x)%R ->
+  round beta fexp Zceil (x + eps) = (x + ulp x)%R.
+Proof with auto with typeclass_instances.
+intros x Zx Fx eps.
+case Zx; intros Zx1.
+(* . 0 < x *)
+intros (Heps1,[Heps2|Heps2]).
+assert (Heps: (0 <= eps < ulp x)%R).
+split.
+now apply Rlt_le.
+exact Heps2.
+assert (Hd := round_DN_plus_eps_pos x Zx Fx eps Heps).
+rewrite round_UP_DN_ulp.
+rewrite Hd.
+rewrite 2!ulp_neq_0.
+unfold canonic_exp.
+now rewrite ln_beta_plus_eps.
+now apply Rgt_not_eq.
+now apply Rgt_not_eq, Rplus_lt_0_compat.
+intros Fs.
+rewrite round_generic in Hd...
+apply Rgt_not_eq with (2 := Hd).
+pattern x at 2 ; rewrite <- Rplus_0_r.
+now apply Rplus_lt_compat_l.
+rewrite Heps2.
+apply round_generic...
+now apply generic_format_succ_aux1.
+(* . x=0 *)
+rewrite <- Zx1, 2!Rplus_0_l.
+intros Heps.
+case (proj2 Heps).
+unfold round, scaled_mantissa, canonic_exp.
+unfold ulp.
+rewrite Req_bool_true; trivial.
+case negligible_exp_spec.
+intros H2.
+intros J; absurd (0 < 0)%R; auto with real.
+apply Rlt_trans with eps; try assumption; apply Heps.
+intros n Hn H.
+assert (fexp (ln_beta beta eps) = fexp n).
+apply valid_exp; try assumption.
+assert(ln_beta beta eps-1 < fexp n)%Z;[idtac|omega].
+apply lt_bpow with beta.
+apply Rle_lt_trans with (2:=H).
+destruct (ln_beta beta eps) as (e,He).
+simpl; rewrite Rabs_pos_eq in He.
+now apply He, Rgt_not_eq.
+now left.
+replace (Zceil (eps * bpow (- fexp (ln_beta beta eps)))) with 1%Z.
+unfold F2R; simpl; rewrite H0; ring.
+apply sym_eq, Zceil_imp.
+split.
+simpl; apply Rmult_lt_0_compat.
+apply Heps.
+apply bpow_gt_0.
+apply Rmult_le_reg_r with (bpow (fexp n)).
+apply bpow_gt_0.
+rewrite Rmult_assoc, <- bpow_plus.
+rewrite H0; ring_simplify (-fexp n + fexp n)%Z.
+simpl; rewrite Rmult_1_l, Rmult_1_r.
+now left.
+intros P; rewrite P.
+apply round_generic...
+apply generic_format_ulp_0.
 Qed.
 
-Theorem round_UP_pred :
-  forall x, (0 < pred x)%R -> F x ->
+
+Theorem round_UP_pred_plus_eps_pos :
+  forall x, (0 < x)%R -> F x ->
   forall eps, (0 < eps <= ulp (pred x) )%R ->
   round beta fexp Zceil (pred x + eps) = x.
 Proof.
 intros x Hx Fx eps Heps.
-rewrite round_UP_succ; trivial.
-apply pred_plus_ulp; trivial.
-apply Rlt_trans with (1:=Hx).
-apply pred_lt_id.
-now apply Rgt_not_eq.
+rewrite round_UP_plus_eps_pos; trivial.
+rewrite pred_eq_pos.
+apply pred_pos_plus_ulp; trivial.
+now left.
+now apply pred_ge_0.
 apply generic_format_pred; trivial.
-apply Rlt_trans with (1:=Hx).
-apply pred_lt_id.
 Qed.
 
-Theorem round_DN_pred :
-  forall x, (0 < pred x)%R -> F x ->
+Theorem round_DN_minus_eps_pos :
+  forall x,  (0 < x)%R -> F x ->
   forall eps, (0 < eps <= ulp (pred x))%R ->
   round beta fexp Zfloor (x - eps) = pred x.
 Proof.
-intros x Hpx Fx eps Heps.
-assert (Hx:(0 < x)%R).
-apply Rlt_trans with (1:=Hpx).
-apply pred_lt_id.
-replace (x-eps)%R with (pred x + (ulp (pred x)-eps))%R.
-2: pattern x at 3; rewrite <- (pred_plus_ulp x); trivial.
+intros x Hpx Fx eps.
+rewrite pred_eq_pos;[intros Heps|now left].
+replace (x-eps)%R with (pred_pos x + (ulp (pred_pos x)-eps))%R.
+2: pattern x at 3; rewrite <- (pred_pos_plus_ulp x); trivial.
 2: ring.
-2: now apply Rgt_not_eq.
-rewrite round_DN_succ; trivial.
-now apply generic_format_pred.
+rewrite round_DN_plus_eps_pos; trivial.
+now apply pred_pos_ge_0.
+now apply generic_format_pred_pos.
 split.
 apply Rle_0_minus.
 now apply Heps.
@@ -1009,15 +1215,96 @@ apply Ropp_lt_contravar.
 now apply Heps.
 Qed.
 
-Lemma le_pred_lt_aux :
+
+Theorem round_DN_plus_eps:
+  forall x, F x ->
+  forall eps, (0 <= eps < if (Rle_bool 0 x) then (ulp x)
+                                     else (ulp (pred (-x))))%R ->
+  round beta fexp Zfloor (x + eps) = x.
+Proof.
+intros x Fx eps Heps.
+case (Rle_or_lt 0 x); intros Zx.
+apply round_DN_plus_eps_pos; try assumption.
+split; try apply Heps.
+rewrite Rle_bool_true in Heps; trivial.
+now apply Heps.
+(* *)
+rewrite Rle_bool_false in Heps; trivial.
+rewrite <- (Ropp_involutive (x+eps)).
+pattern x at 2; rewrite <- (Ropp_involutive x).
+rewrite round_DN_opp.
+apply f_equal.
+replace (-(x+eps))%R with (pred (-x) + (ulp (pred (-x)) - eps))%R.
+rewrite round_UP_pred_plus_eps_pos; try reflexivity.
+now apply Ropp_0_gt_lt_contravar.
+now apply generic_format_opp.
+split.
+apply Rplus_lt_reg_l with eps; ring_simplify.
+apply Heps.
+apply Rplus_le_reg_l with (eps-ulp (pred (- x)))%R; ring_simplify.
+apply Heps.
+unfold pred.
+rewrite Ropp_involutive.
+unfold succ; rewrite Rle_bool_false; try assumption.
+rewrite Ropp_involutive; unfold Rminus.
+rewrite <- Rplus_assoc, pred_pos_plus_ulp.
+ring.
+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)
+                                     else (ulp (pred (-x))))%R ->
+  round beta fexp Zceil (x + eps) = (succ x)%R.
+Proof with auto with typeclass_instances.
+intros x Fx eps Heps.
+case (Rle_or_lt 0 x); intros Zx.
+rewrite succ_eq_pos; try assumption.
+rewrite Rle_bool_true in Heps; trivial.
+apply round_UP_plus_eps_pos; assumption.
+(* *)
+rewrite Rle_bool_false in Heps; trivial.
+rewrite <- (Ropp_involutive (x+eps)).
+rewrite <- (Ropp_involutive (succ x)).
+rewrite round_UP_opp.
+apply f_equal.
+replace (-(x+eps))%R with (-succ x + (-eps + ulp (pred (-x))))%R.
+apply round_DN_plus_eps_pos.
+rewrite <- pred_opp.
+apply pred_ge_0.
+now apply Ropp_0_gt_lt_contravar.
+now apply generic_format_opp.
+now apply generic_format_opp, generic_format_succ.
+split.
+apply Rplus_le_reg_l with eps; ring_simplify.
+apply Heps.
+unfold pred; rewrite Ropp_involutive.
+apply Rplus_lt_reg_l with (eps-ulp (- succ x))%R; ring_simplify.
+apply Heps.
+unfold succ; rewrite Rle_bool_false; try assumption.
+apply trans_eq with (-x +-eps)%R;[idtac|ring].
+pattern (-x)%R at 3; rewrite <- (pred_pos_plus_ulp (-x)).
+rewrite pred_eq_pos.
+ring.
+left; now apply Ropp_0_gt_lt_contravar.
+now apply Ropp_0_gt_lt_contravar.
+now apply generic_format_opp.
+Qed.
+
+
+Lemma le_pred_pos_lt :
   forall x y,
   F x -> F y ->
-  (0 < x < y)%R ->
-  (x <= pred y)%R.
+  (0 <= x < y)%R ->
+  (x <= pred_pos y)%R.
 Proof with auto with typeclass_instances.
-intros x y Hx Hy H.
+intros x y Fx Fy H.
+case (proj1 H); intros V.
 assert (Zy:(0 < y)%R).
-apply Rlt_trans with (1:=proj1 H).
+apply Rle_lt_trans with (1:=proj1 H).
 apply H.
 (* *)
 assert (Zp: (0 < pred y)%R).
@@ -1025,7 +1312,8 @@ assert (Zp:(0 <= pred y)%R).
 apply pred_ge_0 ; trivial.
 destruct Zp; trivial.
 generalize H0.
-unfold pred.
+rewrite pred_eq_pos;[idtac|now left].
+unfold pred_pos.
 destruct (ln_beta beta y) as (ey,Hey); simpl.
 case Req_bool_spec; intros Hy2.
 (* . *)
@@ -1058,7 +1346,7 @@ absurd (0 < Ztrunc (scaled_mantissa beta fexp x) < 1)%Z.
 omega.
 split.
 apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
-now rewrite <- Hx.
+now rewrite <- Fx.
 apply lt_Z2R.
 apply Rmult_lt_reg_r with (bpow (canonic_exp beta fexp x)).
 apply bpow_gt_0.
@@ -1082,7 +1370,8 @@ intros Hy3.
 assert (y = bpow (fexp ey))%R.
 apply Rminus_diag_uniq.
 rewrite Hy3.
-unfold ulp, canonic_exp.
+rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq].
+unfold canonic_exp.
 rewrite (ln_beta_unique beta y ey); trivial.
 apply Hey.
 now apply Rgt_not_eq.
@@ -1104,68 +1393,701 @@ apply ln_beta_unique.
 apply Hey.
 now apply Rgt_not_eq.
 (* *)
-case (Rle_or_lt (ulp (pred y)) (y-x)); intros H1.
+case (Rle_or_lt (ulp (pred_pos y)) (y-x)); intros H1.
 (* . *)
-apply Rplus_le_reg_r with (-x + ulp (pred y))%R.
-ring_simplify (x+(-x+ulp (pred y)))%R.
+apply Rplus_le_reg_r with (-x + ulp (pred_pos y))%R.
+ring_simplify (x+(-x+ulp (pred_pos y)))%R.
 apply Rle_trans with (1:=H1).
-rewrite <- (pred_plus_ulp y) at 1; trivial.
+rewrite <- (pred_pos_plus_ulp y) at 1; trivial.
 apply Req_le; ring.
-now apply Rgt_not_eq.
 (* . *)
 replace x with (y-(y-x))%R by ring.
-rewrite <- round_DN_pred with (eps:=(y-x)%R); try easy.
+rewrite <- pred_eq_pos;[idtac|now left].
+rewrite <- round_DN_minus_eps_pos with (eps:=(y-x)%R); try easy.
 ring_simplify (y-(y-x))%R.
 apply Req_le.
 apply sym_eq.
 apply round_generic...
 split; trivial.
 now apply Rlt_Rminus.
+rewrite pred_eq_pos;[idtac|now left].
 now apply Rlt_le.
+rewrite <- V; apply pred_pos_ge_0; trivial.
+apply Rle_lt_trans with (1:=proj1 H); apply H.
+Qed.
+
+Theorem succ_le_lt_aux:
+  forall x y,
+  F x -> F y ->
+  (0 <= x)%R -> (x < y)%R ->
+  (succ x <= y)%R.
+Proof with auto with typeclass_instances.
+intros x y Hx Hy Zx H.
+rewrite succ_eq_pos; trivial.
+case (Rle_or_lt (ulp x) (y-x)); intros H1.
+apply Rplus_le_reg_r with (-x)%R.
+now ring_simplify (x+ulp x + -x)%R.
+replace y with (x+(y-x))%R by ring.
+absurd (x < y)%R.
+2: apply H.
+apply Rle_not_lt; apply Req_le.
+rewrite <- round_DN_plus_eps_pos with (eps:=(y-x)%R); try easy.
+ring_simplify (x+(y-x))%R.
+apply sym_eq.
+apply round_generic...
+split; trivial.
+apply Rlt_le; now apply Rlt_Rminus.
+Qed.
+
+Theorem succ_le_lt:
+  forall x y,
+  F x -> F y ->
+  (x < y)%R ->
+  (succ x <= y)%R.
+Proof with auto with typeclass_instances.
+intros x y Fx Fy H.
+destruct (Rle_or_lt 0 x) as [Hx|Hx].
+now apply succ_le_lt_aux.
+unfold succ; rewrite Rle_bool_false; try assumption.
+case (Rle_or_lt y 0); intros Hy.
+rewrite <- (Ropp_involutive y).
+apply Ropp_le_contravar.
+apply le_pred_pos_lt.
+now apply generic_format_opp.
+now apply generic_format_opp.
+split.
+rewrite <- Ropp_0; now apply Ropp_le_contravar.
+now apply Ropp_lt_contravar.
+apply Rle_trans with (-0)%R.
+apply Ropp_le_contravar.
+apply pred_pos_ge_0.
+rewrite <- Ropp_0; now apply Ropp_lt_contravar.
+now apply generic_format_opp.
+rewrite Ropp_0; now left.
 Qed.
 
 Theorem le_pred_lt :
   forall x y,
   F x -> F y ->
-  (0 < y)%R ->
   (x < y)%R ->
   (x <= pred y)%R.
 Proof.
-intros x y Fx Fy Hy Hxy.
-destruct (Rle_or_lt x 0) as [Hx|Hx].
-apply Rle_trans with (1 := Hx).
-now apply pred_ge_0.
-apply le_pred_lt_aux ; try easy.
-now split.
+intros x y Fx Fy Hxy.
+rewrite <- (Ropp_involutive x).
+unfold pred; apply Ropp_le_contravar.
+apply succ_le_lt.
+now apply generic_format_opp.
+now apply generic_format_opp.
+now apply Ropp_lt_contravar.
 Qed.
 
 
-Theorem pred_succ : forall { monotone_exp : Monotone_exp fexp },
-  forall x, F x -> (0 < x)%R -> pred (x + ulp x)=x.
+Theorem lt_succ_le:
+  forall x y,
+  F x -> F y -> (y <> 0)%R ->
+  (x <= y)%R ->
+  (x < succ y)%R.
 Proof.
-intros L x Fx Hx.
-assert (x <= pred (x + ulp x))%R.
-apply le_pred_lt.
-assumption.
-now apply generic_format_succ.
-replace 0%R with (0+0)%R by ring; apply Rplus_lt_compat; try apply Hx.
+intros x y Fx Fy Zy Hxy.
+case (Rle_or_lt (succ y) x); trivial; intros H.
+absurd (succ y = y)%R.
+apply Rgt_not_eq.
+now apply succ_gt_id.
+apply Rle_antisym.
+now apply Rle_trans with x.
+apply succ_ge_id.
+Qed.
+
+
+Theorem succ_pred_aux : forall x, F x -> (0 < x)%R -> succ (pred x)=x.
+Proof.
+intros x Fx Hx.
+rewrite pred_eq_pos;[idtac|now left].
+rewrite succ_eq_pos.
+2: now apply pred_pos_ge_0.
+now apply pred_pos_plus_ulp.
+Qed.
+
+Theorem pred_succ_aux_0 : (pred (succ 0)=0)%R.
+Proof.
+unfold succ; rewrite Rle_bool_true.
+2: apply Rle_refl.
+rewrite Rplus_0_l.
+rewrite pred_eq_pos.
+2: apply ulp_ge_0.
+unfold ulp; rewrite Req_bool_true; trivial.
+case negligible_exp_spec'.
+(* *)
+intros (H1,H2); rewrite H1.
+unfold pred_pos; rewrite Req_bool_false.
+2: apply Rlt_not_eq, bpow_gt_0.
+unfold ulp; rewrite Req_bool_true; trivial.
+rewrite H1; ring.
+(* *)
+intros (n,(H1,H2)); rewrite H1.
+unfold pred_pos.
+rewrite ln_beta_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.
+Qed.
+
+Theorem pred_succ_aux : forall x, F x -> (0 < x)%R -> pred (succ x)=x.
+Proof.
+intros x Fx Hx.
+rewrite succ_eq_pos;[idtac|now left].
+rewrite pred_eq_pos.
+2: apply Rplus_le_le_0_compat;[now left| apply ulp_ge_0].
+unfold pred_pos.
+case Req_bool_spec; intros H1.
+(* *)
+pose (l:=(ln_beta beta (x+ulp x))).
+rewrite H1 at 1; fold l.
+apply Rplus_eq_reg_r with (ulp x).
+rewrite H1; fold l.
+rewrite (ulp_neq_0 x) at 3.
+2: now apply Rgt_not_eq.
+unfold canonic_exp.
+replace (fexp (ln_beta beta x)) with (fexp (l-1))%Z.
+ring.
+apply f_equal, sym_eq.
+apply Zle_antisym.
+assert (ln_beta beta x - 1 < l - 1)%Z;[idtac|omega].
+apply lt_bpow with beta.
+unfold l; rewrite <- H1.
+apply Rle_lt_trans with x.
+destruct (ln_beta beta x) as (e,He); simpl.
+rewrite <- (Rabs_right x) at 1.
+2: apply Rle_ge; now left.
+now apply He, Rgt_not_eq.
+apply Rplus_lt_reg_l with (-x)%R; ring_simplify.
+rewrite ulp_neq_0.
 apply bpow_gt_0.
-apply Rplus_lt_reg_r with (-x)%R; ring_simplify.
+now apply Rgt_not_eq.
+apply le_bpow with beta.
+unfold l; rewrite <- H1.
+apply id_p_ulp_le_bpow; trivial.
+rewrite <- (Rabs_right x) at 1.
+2: apply Rle_ge; now left.
+apply bpow_ln_beta_gt.
+(* *)
+replace (ulp (x+ ulp x)) with (ulp x).
+ring.
+rewrite ulp_neq_0 at 1.
+2: now apply Rgt_not_eq.
+rewrite ulp_neq_0 at 1.
+2: apply Rgt_not_eq, Rlt_gt.
+2: apply Rlt_le_trans with (1:=Hx).
+2: apply Rplus_le_reg_l with (-x)%R; ring_simplify.
+2: apply ulp_ge_0.
+apply f_equal; unfold canonic_exp; apply f_equal.
+apply sym_eq, ln_beta_unique.
+rewrite Rabs_right.
+2: apply Rle_ge; left.
+2: apply Rlt_le_trans with (1:=Hx).
+2: apply Rplus_le_reg_l with (-x)%R; ring_simplify.
+2: apply ulp_ge_0.
+destruct (ln_beta beta x) as (e,He); simpl.
+rewrite Rabs_right in He.
+2: apply Rle_ge; now left.
+split.
+apply Rle_trans with x.
+apply He, Rgt_not_eq; assumption.
+apply Rplus_le_reg_l with (-x)%R; ring_simplify.
+apply ulp_ge_0.
+case (Rle_lt_or_eq_dec (x+ulp x) (bpow e)); trivial.
+apply id_p_ulp_le_bpow; trivial.
+apply He, Rgt_not_eq; assumption.
+intros K; contradict H1.
+rewrite K, ln_beta_bpow.
+apply f_equal; ring.
+Qed.
+
+
+
+Theorem succ_pred : forall x, F x -> succ (pred x)=x.
+Proof.
+intros x Fx.
+case (Rle_or_lt 0 x); intros Hx.
+destruct Hx as [Hx|Hx].
+now apply succ_pred_aux.
+rewrite <- Hx.
+rewrite pred_eq_opp_succ_opp, succ_opp, Ropp_0.
+rewrite pred_succ_aux_0; ring.
+rewrite pred_eq_opp_succ_opp, succ_opp.
+rewrite pred_succ_aux.
+ring.
+now apply generic_format_opp.
+now apply Ropp_0_gt_lt_contravar.
+Qed.
+
+Theorem pred_succ : forall x, F x -> pred (succ x)=x.
+Proof.
+intros x Fx.
+case (Rle_or_lt 0 x); intros Hx.
+destruct Hx as [Hx|Hx].
+now apply pred_succ_aux.
+rewrite <- Hx.
+apply pred_succ_aux_0.
+rewrite succ_eq_opp_pred_opp, pred_opp.
+rewrite succ_pred_aux.
+ring.
+now apply generic_format_opp.
+now apply Ropp_0_gt_lt_contravar.
+Qed.
+
+
+Theorem round_UP_pred_plus_eps :
+  forall x, F x ->
+  forall eps, (0 < eps <= if (Rle_bool x 0) then (ulp x)
+                                     else (ulp (pred x)))%R ->
+  round beta fexp Zceil (pred x + eps) = x.
+Proof.
+intros x Fx eps Heps.
+rewrite round_UP_plus_eps.
+now apply succ_pred.
+now apply generic_format_pred.
+unfold pred at 4.
+rewrite Ropp_involutive, pred_succ.
+rewrite ulp_opp.
+generalize Heps; case (Rle_bool_spec x 0); intros H1 H2.
+rewrite Rle_bool_false; trivial.
+case H1; intros H1'.
+apply Rlt_le_trans with (2:=H1).
+apply pred_lt_id.
+now apply Rlt_not_eq.
+rewrite H1'; unfold pred, succ.
+rewrite Ropp_0; rewrite Rle_bool_true;[idtac|now right].
+rewrite Rplus_0_l.
+rewrite <- Ropp_0; apply Ropp_lt_contravar.
+apply Rlt_le_trans with (1:=proj1 H2).
+apply Rle_trans with (1:=proj2 H2).
+rewrite Ropp_0, H1'.
+now right.
+rewrite Rle_bool_true; trivial.
+now apply pred_ge_0.
+now apply generic_format_opp.
+Qed.
+
+
+Theorem round_DN_minus_eps:
+  forall x,  F x ->
+  forall eps, (0 < eps <= if (Rle_bool x 0) then (ulp x)
+                                     else (ulp (pred x)))%R ->
+  round beta fexp Zfloor (x - eps) = pred x.
+Proof.
+intros x Fx eps Heps.
+replace (x-eps)%R with (-(-x+eps))%R by ring.
+rewrite round_DN_opp.
+unfold pred; apply f_equal.
+pattern (-x)%R at 1; rewrite <- (pred_succ (-x)).
+apply round_UP_pred_plus_eps.
+now apply generic_format_succ, generic_format_opp.
+rewrite pred_succ.
+rewrite ulp_opp.
+generalize Heps; case (Rle_bool_spec x 0); intros H1 H2.
+rewrite Rle_bool_false; trivial.
+case H1; intros H1'.
+apply Rlt_le_trans with (-x)%R.
+now apply Ropp_0_gt_lt_contravar.
+apply succ_ge_id.
+rewrite H1', Ropp_0, succ_eq_pos;[idtac|now right].
+rewrite Rplus_0_l.
+apply Rlt_le_trans with (1:=proj1 H2).
+rewrite H1' in H2; apply H2.
+rewrite Rle_bool_true.
+now rewrite succ_opp, ulp_opp.
+rewrite succ_opp.
+rewrite <- Ropp_0; apply Ropp_le_contravar.
+now apply pred_ge_0.
+now apply generic_format_opp.
+now apply generic_format_opp.
+Qed.
+
+(** Error of a rounding, expressed in number of ulps *)
+(** false for x=0 in the FLX format *)
+(* was ulp_error *)
+Theorem error_lt_ulp :
+  forall rnd { Zrnd : Valid_rnd rnd } x,
+   (x <> 0)%R ->
+  (Rabs (round beta fexp rnd x - x) < ulp x)%R.
+Proof with auto with typeclass_instances.
+intros rnd Zrnd x Zx.
+destruct (generic_format_EM beta fexp x) as [Hx|Hx].
+(* x = rnd x *)
+rewrite round_generic...
+unfold Rminus.
+rewrite Rplus_opp_r, Rabs_R0.
+rewrite ulp_neq_0; trivial.
 apply bpow_gt_0.
-apply Rle_antisym; trivial.
-apply Rplus_le_reg_r with (ulp (pred (x + ulp x))).
-rewrite pred_plus_ulp.
-apply Rplus_le_compat_l.
-now apply ulp_le.
-replace 0%R with (0+0)%R by ring; apply Rplus_lt_compat; try apply Hx.
+(* x <> rnd x *)
+destruct (round_DN_or_UP beta fexp rnd x) as [H|H] ; rewrite H ; clear H.
+(* . *)
+rewrite Rabs_left1.
+rewrite Ropp_minus_distr.
+apply Rplus_lt_reg_l with (round beta fexp Zfloor x).
+rewrite <- round_UP_DN_ulp with (1 := Hx).
+ring_simplify.
+assert (Hu: (x <= round beta fexp Zceil x)%R).
+apply round_UP_pt...
+destruct Hu as [Hu|Hu].
+exact Hu.
+elim Hx.
+rewrite Hu.
+apply generic_format_round...
+apply Rle_minus.
+apply round_DN_pt...
+(* . *)
+rewrite Rabs_pos_eq.
+rewrite round_UP_DN_ulp with (1 := Hx).
+apply Rplus_lt_reg_r with (x - ulp x)%R.
+ring_simplify.
+assert (Hd: (round beta fexp Zfloor x <= x)%R).
+apply round_DN_pt...
+destruct Hd as [Hd|Hd].
+exact Hd.
+elim Hx.
+rewrite <- Hd.
+apply generic_format_round...
+apply Rle_0_minus.
+apply round_UP_pt...
+Qed.
+
+(* was ulp_error_le *)
+Theorem error_le_ulp :
+  forall rnd { Zrnd : Valid_rnd rnd } x,
+  (Rabs (round beta fexp rnd x - x) <= ulp x)%R.
+Proof with auto with typeclass_instances.
+intros  rnd Zrnd x.
+case (Req_dec x 0).
+intros Zx; rewrite Zx, round_0...
+unfold Rminus; rewrite Rplus_0_l, Ropp_0, Rabs_R0.
+apply ulp_ge_0.
+intros Zx; left.
+now apply error_lt_ulp.
+Qed.
+
+(* was ulp_half_error *)
+Theorem error_le_half_ulp :
+  forall choice x,
+  (Rabs (round beta fexp (Znearest choice) x - x) <= /2 * ulp x)%R.
+Proof with auto with typeclass_instances.
+intros choice x.
+destruct (generic_format_EM beta fexp x) as [Hx|Hx].
+(* x = rnd x *)
+rewrite round_generic...
+unfold Rminus.
+rewrite Rplus_opp_r, Rabs_R0.
+apply Rmult_le_pos.
+apply Rlt_le.
+apply Rinv_0_lt_compat.
+now apply (Z2R_lt 0 2).
+apply ulp_ge_0.
+(* x <> rnd x *)
+set (d := round beta fexp Zfloor x).
+destruct (round_N_pt beta fexp choice x) as (Hr1, Hr2).
+destruct (Rle_or_lt (x - d) (d + ulp x - x)) as [H|H].
+(* . rnd(x) = rndd(x) *)
+apply Rle_trans with (Rabs (d - x)).
+apply Hr2.
+apply (round_DN_pt beta fexp x).
+rewrite Rabs_left1.
+rewrite Ropp_minus_distr.
+apply Rmult_le_reg_r with 2%R.
+now apply (Z2R_lt 0 2).
+apply Rplus_le_reg_r with (d - x)%R.
+ring_simplify.
+apply Rle_trans with (1 := H).
+right. field.
+apply Rle_minus.
+apply (round_DN_pt beta fexp x).
+(* . rnd(x) = rndu(x) *)
+assert (Hu: (d + ulp x)%R = round beta fexp Zceil x).
+unfold d.
+now rewrite <- round_UP_DN_ulp.
+apply Rle_trans with (Rabs (d + ulp x - x)).
+apply Hr2.
+rewrite Hu.
+apply (round_UP_pt beta fexp x).
+rewrite Rabs_pos_eq.
+apply Rmult_le_reg_r with 2%R.
+now apply (Z2R_lt 0 2).
+apply Rplus_le_reg_r with (- (d + ulp x - x))%R.
+ring_simplify.
+apply Rlt_le.
+apply Rlt_le_trans with (1 := H).
+right. field.
+apply Rle_0_minus.
+rewrite Hu.
+apply (round_UP_pt beta fexp x).
+Qed.
+
+
+Theorem ulp_DN :
+  forall x,
+  (0 < round beta fexp Zfloor x)%R ->
+  ulp (round beta fexp Zfloor x) = ulp x.
+Proof with auto with typeclass_instances.
+intros x Hd.
+rewrite 2!ulp_neq_0.
+now rewrite canonic_exp_DN with (2 := Hd).
+intros T; contradict Hd; rewrite T, round_0...
+apply Rlt_irrefl.
+now apply Rgt_not_eq.
+Qed.
+
+Theorem round_neq_0_negligible_exp:
+    negligible_exp=None -> forall rnd { Zrnd : Valid_rnd rnd } x,
+   (x <> 0)%R ->  (round beta fexp rnd x <> 0)%R.
+Proof with auto with typeclass_instances.
+intros H rndn Hrnd x Hx K.
+case negligible_exp_spec'.
+intros (_,Hn).
+destruct (ln_beta beta x) as (e,He).
+absurd (fexp e < e)%Z.
+apply Zle_not_lt.
+apply exp_small_round_0 with beta rndn x...
+apply (Hn e).
+intros (n,(H1,_)).
+rewrite H in H1; discriminate.
+Qed.
+
+
+(** allows rnd x to be 0 *)
+(* was ulp_error_f *)
+Theorem error_lt_ulp_round :
+  forall { Hm : Monotone_exp fexp } rnd { Zrnd : Valid_rnd rnd } x,
+  ( x <> 0)%R ->
+  (Rabs (round beta fexp rnd x - x) < ulp (round beta fexp rnd x))%R.
+Proof with auto with typeclass_instances.
+intros Hm.
+(* wlog *)
+cut (forall rnd : R -> Z, Valid_rnd rnd -> forall x : R, (0 < x)%R  ->
+    (Rabs (round beta fexp rnd x - x) < ulp (round beta fexp rnd x))%R).
+intros M rnd Hrnd x Zx.
+case (Rle_or_lt 0 x).
+intros H; destruct H.
+now apply M.
+contradict H; now apply sym_not_eq.
+intros H.
+rewrite <- (Ropp_involutive x).
+rewrite round_opp, ulp_opp.
+replace (- round beta fexp (Zrnd_opp rnd) (- x) - - - x)%R with
+    (-(round beta fexp (Zrnd_opp rnd) (- x) - (-x)))%R by ring.
+rewrite Rabs_Ropp.
+apply M.
+now apply valid_rnd_opp.
+now apply Ropp_0_gt_lt_contravar.
+(* 0 < x *)
+intros rnd Hrnd x Hx.
+case (Rle_lt_or_eq_dec 0 (round beta fexp Zfloor x)).
+apply round_ge_generic...
+apply generic_format_0.
+now left.
+(* . 0 < round Zfloor x *)
+intros Hx2.
+apply Rlt_le_trans with (ulp x).
+apply error_lt_ulp...
+now apply Rgt_not_eq.
+rewrite <- ulp_DN; trivial.
+apply ulp_le_pos.
+now left.
+case (round_DN_or_UP beta fexp rnd x); intros V; rewrite V.
+apply Rle_refl.
+apply Rle_trans with x.
+apply round_DN_pt...
+apply round_UP_pt...
+(* . 0 = round Zfloor x *)
+intros Hx2.
+case (round_DN_or_UP beta fexp rnd x); intros V; rewrite V; clear V.
+(* .. round down -- difficult case *)
+rewrite <- Hx2.
+unfold Rminus; rewrite Rplus_0_l, Rabs_Ropp.
+unfold ulp; rewrite Req_bool_true; trivial.
+case negligible_exp_spec.
+(* without minimal exponent *)
+intros K; contradict Hx2.
+apply Rlt_not_eq.
+apply F2R_gt_0_compat; simpl.
+apply Zlt_le_trans with 1%Z.
+apply Pos2Z.is_pos.
+apply Zfloor_lub.
+simpl; unfold scaled_mantissa, canonic_exp.
+destruct (ln_beta beta x) as (e,He); simpl.
+apply Rle_trans with (bpow (e-1) * bpow (- fexp e))%R.
+rewrite <- bpow_plus.
+replace 1%R with (bpow 0) by reflexivity.
+apply bpow_le.
+specialize (K e); omega.
+apply Rmult_le_compat_r.
+apply bpow_ge_0.
+rewrite <- (Rabs_pos_eq x).
+now apply He, Rgt_not_eq.
+now left.
+(* with a minimal exponent *)
+intros n Hn.
+rewrite Rabs_pos_eq;[idtac|now left].
+case (Rle_or_lt (bpow (fexp n)) x); trivial.
+intros K; contradict Hx2.
+apply Rlt_not_eq.
+apply Rlt_le_trans with (bpow (fexp n)).
 apply bpow_gt_0.
-now apply generic_format_succ.
-apply Rgt_not_eq.
-now apply Rlt_le_trans with x.
+apply round_ge_generic...
+apply generic_format_bpow.
+now apply valid_exp.
+(* .. round up *)
+apply Rlt_le_trans with (ulp x).
+apply error_lt_ulp...
+now apply Rgt_not_eq.
+apply ulp_le_pos.
+now left.
+apply round_UP_pt...
+Qed.
+
+(** allows both x and rnd x to be 0 *)
+(* was ulp_half_error_f *)
+Theorem error_le_half_ulp_round :
+  forall { Hm : Monotone_exp fexp },
+  forall choice x,
+  (Rabs (round beta fexp (Znearest choice) x - x) <= /2 * ulp (round beta fexp (Znearest choice) x))%R.
+Proof with auto with typeclass_instances.
+intros Hm choice x.
+case (Req_dec (round beta fexp (Znearest choice) x) 0); intros Hfx.
+(* *)
+case (Req_dec x 0); intros Hx.
+apply Rle_trans with (1:=error_le_half_ulp _ _).
+rewrite Hx, round_0...
+right; ring.
+generalize (error_le_half_ulp choice x).
+rewrite Hfx.
+unfold Rminus; rewrite Rplus_0_l, Rabs_Ropp.
+intros N.
+unfold ulp; rewrite Req_bool_true; trivial.
+case negligible_exp_spec'.
+intros (H1,H2).
+contradict Hfx.
+apply round_neq_0_negligible_exp...
+intros (n,(H1,Hn)); rewrite H1.
+apply Rle_trans with (1:=N).
+right; apply f_equal.
+rewrite ulp_neq_0; trivial.
+apply f_equal.
+unfold canonic_exp.
+apply valid_exp; trivial.
+assert (ln_beta beta x -1 < fexp n)%Z;[idtac|omega].
+apply lt_bpow with beta.
+destruct (ln_beta beta x) as (e,He).
+simpl.
+apply Rle_lt_trans with (Rabs x).
+now apply He.
+apply Rle_lt_trans with (Rabs (round beta fexp (Znearest choice) x - x)).
+right; rewrite Hfx; unfold Rminus; rewrite Rplus_0_l.
+apply sym_eq, Rabs_Ropp.
+apply Rlt_le_trans with (ulp 0).
+rewrite <- Hfx.
+apply error_lt_ulp_round...
+unfold ulp; rewrite Req_bool_true, H1; trivial.
+now right.
+(* *)
+case (round_DN_or_UP beta fexp (Znearest choice) x); intros Hx.
+(* . *)
+case (Rle_or_lt 0 (round beta fexp Zfloor x)).
+intros H; destruct H.
+rewrite Hx at 2.
+rewrite ulp_DN; trivial.
+apply error_le_half_ulp.
+rewrite Hx in Hfx; contradict Hfx; auto with real.
+intros H.
+apply Rle_trans with (1:=error_le_half_ulp _ _).
+apply Rmult_le_compat_l.
+auto with real.
+apply ulp_le.
+rewrite Hx; rewrite (Rabs_left1 x), Rabs_left; try assumption.
+apply Ropp_le_contravar.
+apply (round_DN_pt beta fexp x).
+case (Rle_or_lt x 0); trivial.
+intros H1; contradict H.
+apply Rle_not_lt.
+apply round_ge_generic...
+apply generic_format_0.
+now left.
+(* . *)
+case (Rle_or_lt 0 (round beta fexp Zceil x)).
+intros H; destruct H.
+apply Rle_trans with (1:=error_le_half_ulp _ _).
+apply Rmult_le_compat_l.
+auto with real.
+apply ulp_le_pos; trivial.
+case (Rle_or_lt 0 x); trivial.
+intros H1; contradict H.
+apply Rle_not_lt.
+apply round_le_generic...
+apply generic_format_0.
+now left.
+rewrite Hx; apply (round_UP_pt beta fexp x).
+rewrite Hx in Hfx; contradict Hfx; auto with real.
+intros H.
+rewrite Hx at 2; rewrite <- (ulp_opp (round beta fexp Zceil x)).
+rewrite <- round_DN_opp.
+rewrite ulp_DN; trivial.
+pattern x at 1 2; rewrite <- Ropp_involutive.
+rewrite round_N_opp.
+unfold Rminus.
+rewrite <- Ropp_plus_distr, Rabs_Ropp.
+apply error_le_half_ulp.
+rewrite round_DN_opp; apply Ropp_0_gt_lt_contravar; apply Rlt_gt; assumption.
 Qed.
 
 
-Theorem lt_UP_le_DN :
+Theorem pred_le: forall x y,
+   F x -> F y -> (x <= y)%R -> (pred x <= pred y)%R.
+Proof.
+intros x y Fx Fy Hxy.
+assert (V:( ((x = 0) /\ (y = 0)) \/ (x <>0 \/ x < y))%R).
+case (Req_dec x 0); intros Zx.
+case Hxy; intros Zy.
+now right; right.
+left; split; trivial; now rewrite <- Zy.
+now right; left.
+destruct V as [(V1,V2)|V].
+rewrite V1,V2; now right.
+apply le_pred_lt; try assumption.
+apply generic_format_pred; try assumption.
+case V; intros V1.
+apply Rlt_le_trans with (2:=Hxy).
+now apply pred_lt_id.
+apply Rle_lt_trans with (2:=V1).
+now apply pred_le_id.
+Qed.
+
+Theorem succ_le: forall x y,
+   F x -> F y -> (x <= y)%R -> (succ x <= succ y)%R.
+Proof.
+intros x y Fx Fy Hxy.
+rewrite 2!succ_eq_opp_pred_opp.
+apply Ropp_le_contravar, pred_le; try apply generic_format_opp; try assumption.
+now apply Ropp_le_contravar.
+Qed.
+
+Theorem pred_le_inv: forall x y, F x -> F y
+   -> (pred x <= pred y)%R -> (x <= y)%R.
+Proof.
+intros x y Fx Fy Hxy.
+rewrite <- (succ_pred x), <- (succ_pred y); try assumption.
+apply succ_le; trivial; now apply generic_format_pred.
+Qed.
+
+Theorem succ_le_inv: forall x y, F x -> F y
+   -> (succ x <= succ y)%R -> (x <= y)%R.
+Proof.
+intros x y Fx Fy Hxy.
+rewrite <- (pred_succ x), <- (pred_succ y); try assumption.
+apply pred_le; trivial; now apply generic_format_succ.
+Qed.
+
+(* was lt_UP_le_DN *)
+Theorem le_round_DN_lt_UP :
   forall x y, F y ->
   (y < round beta fexp Zceil x -> y <= round beta fexp Zfloor x)%R.
 Proof with auto with typeclass_instances.
@@ -1178,26 +2100,58 @@ apply round_UP_pt...
 now apply Rlt_le.
 Qed.
 
+(* was lt_DN_le_UP *)
+Theorem round_UP_le_gt_DN :
+  forall x y, F y ->
+   (round beta fexp Zfloor x < y -> round beta fexp Zceil x <= y)%R.
+Proof with auto with typeclass_instances.
+intros x y Fy Hlt.
+apply round_UP_pt...
+apply Rnot_lt_le.
+contradict Hlt.
+apply RIneq.Rle_not_lt.
+apply round_DN_pt...
+now apply Rlt_le.
+Qed.
+
+
+
 Theorem pred_UP_le_DN :
-  forall x, (0 < round beta fexp Zceil x)%R ->
-  (pred (round beta fexp Zceil x) <= round beta fexp Zfloor x)%R.
+  forall x, (pred (round beta fexp Zceil x) <= round beta fexp Zfloor x)%R.
 Proof with auto with typeclass_instances.
-intros x Pxu.
+intros x.
 destruct (generic_format_EM beta fexp x) as [Fx|Fx].
 rewrite !round_generic...
-now apply Rlt_le; apply pred_lt_id.
+apply pred_le_id.
+case (Req_dec (round beta fexp Zceil x) 0); intros Zx.
+rewrite Zx; unfold pred; rewrite Ropp_0.
+unfold succ; rewrite Rle_bool_true;[idtac|now right].
+rewrite Rplus_0_l; unfold ulp; rewrite Req_bool_true; trivial.
+case negligible_exp_spec'.
+intros (H1,H2).
+contradict Zx; apply round_neq_0_negligible_exp...
+intros L; apply Fx; rewrite L; apply generic_format_0.
+intros (n,(H1,Hn)); rewrite H1.
+case (Rle_or_lt (- bpow (fexp n)) (round beta fexp Zfloor x)); trivial; intros K.
+absurd (round beta fexp Zceil x <= - bpow (fexp n))%R.
+apply Rlt_not_le.
+rewrite Zx, <- Ropp_0.
+apply Ropp_lt_contravar, bpow_gt_0.
+apply round_UP_le_gt_DN; try assumption.
+apply generic_format_opp, generic_format_bpow.
+now apply valid_exp.
 assert (let u := round beta fexp Zceil x in pred u < u)%R as Hup.
-  now apply pred_lt_id.
-apply lt_UP_le_DN...
+now apply pred_lt_id.
+apply le_round_DN_lt_UP...
 apply generic_format_pred...
 now apply round_UP_pt.
 Qed.
 
 Theorem pred_UP_eq_DN :
-  forall x, (0 < round beta fexp Zceil x)%R -> ~ F x ->
+  forall x,  ~ F x ->
   (pred (round beta fexp Zceil x) = round beta fexp Zfloor x)%R.
 Proof with auto with typeclass_instances.
-intros x Px Fx.
+intros x Fx.
 apply Rle_antisym.
 now apply pred_UP_le_DN.
 apply le_pred_lt; try apply generic_format_round...
@@ -1205,212 +2159,200 @@ pose proof round_DN_UP_lt _ _ _ Fx as HE.
 now apply Rlt_trans with (1 := proj1 HE) (2 := proj2 HE).
 Qed.
 
+Theorem succ_DN_eq_UP :
+  forall x,  ~ F x ->
+  (succ (round beta fexp Zfloor x) = round beta fexp Zceil x)%R.
+Proof with auto with typeclass_instances.
+intros x Fx.
+rewrite <- pred_UP_eq_DN; trivial.
+rewrite succ_pred; trivial.
+apply generic_format_round...
+Qed.
+
+
+(* was betw_eq_DN *)
+Theorem round_DN_eq_betw: forall x d, F d
+     -> (d <= x < succ d)%R
+        -> round beta fexp Zfloor x = d.
+Proof with auto with typeclass_instances.
+intros x d Fd (Hxd1,Hxd2).
+generalize (round_DN_pt beta fexp x); intros (T1,(T2,T3)).
+apply sym_eq, Rle_antisym.
+now apply T3.
+destruct (generic_format_EM beta fexp x) as [Fx|NFx].
+rewrite round_generic...
+apply succ_le_inv; try assumption.
+apply succ_le_lt; try assumption.
+apply generic_format_succ...
+apply succ_le_inv; try assumption.
+rewrite succ_DN_eq_UP; trivial.
+apply round_UP_pt...
+apply generic_format_succ...
+now left.
+Qed.
+
+(* was betw_eq_UP *)
+Theorem round_UP_eq_betw: forall x u, F u
+    -> (pred u < x <= u)%R
+    -> round beta fexp Zceil x = u.
+Proof with auto with typeclass_instances.
+intros x u Fu Hux.
+rewrite <- (Ropp_involutive (round beta fexp Zceil x)).
+rewrite <- round_DN_opp.
+rewrite <- (Ropp_involutive u).
+apply f_equal.
+apply round_DN_eq_betw; try assumption.
+now apply generic_format_opp.
+split;[now apply Ropp_le_contravar|idtac].
+rewrite succ_opp.
+now apply Ropp_lt_contravar.
+Qed.
 
 
 
 
 (** Properties of rounding to nearest and ulp *)
 
-Theorem rnd_N_le_half_an_ulp: forall choice u v,
-  F u -> (0 < u)%R -> (v < u + (ulp u)/2)%R
+Theorem round_N_le_midp: forall choice u v,
+  F u -> (v < (u + succ u)/2)%R
       -> (round beta fexp (Znearest choice)  v <= u)%R.
 Proof with auto with typeclass_instances.
-intros choice u v Fu Hu H.
+intros choice u v Fu H.
 (* . *)
-assert (0 < ulp u / 2)%R.
-unfold Rdiv; apply Rmult_lt_0_compat.
-unfold ulp; apply bpow_gt_0.
-auto with real.
-(* . *)
-assert (ulp u / 2 < ulp u)%R.
-apply Rlt_le_trans with (ulp u *1)%R;[idtac|right; ring].
-unfold Rdiv; apply Rmult_lt_compat_l.
-apply bpow_gt_0.
+assert (V: ((succ u = 0 /\ u = 0) \/ u < succ u)%R).
+specialize (succ_ge_id u); intros P; destruct P as [P|P].
+now right.
+case (Req_dec u 0); intros Zu.
+left; split; trivial.
+now rewrite <- P.
+right; now apply succ_gt_id.
+(* *)
+destruct V as [(V1,V2)|V].
+rewrite V2; apply round_le_generic...
+apply generic_format_0.
+left; apply Rlt_le_trans with (1:=H).
+rewrite V1,V2; right; field.
+(* *)
+assert (T: (u < (u + succ u) / 2 < succ u)%R).
+split.
 apply Rmult_lt_reg_l with 2%R.
-auto with real.
-apply Rle_lt_trans with 1%R.
+now auto with real.
+apply Rplus_lt_reg_l with (-u)%R.
+apply Rle_lt_trans with u;[right; ring|idtac].
+apply Rlt_le_trans with (1:=V).
 right; field.
-rewrite Rmult_1_r; auto with real.
+apply Rmult_lt_reg_l with 2%R.
+now auto with real.
+apply Rplus_lt_reg_l with (-succ u)%R.
+apply Rle_lt_trans with u;[right; field|idtac].
+apply Rlt_le_trans with (1:=V).
+right; ring.
 (* *)
-apply Rnd_N_pt_monotone with F v (u + ulp u / 2)%R...
+destruct T as (T1,T2).
+apply Rnd_N_pt_monotone with F v ((u + succ u) / 2)%R...
 apply round_N_pt...
-apply Rnd_DN_pt_N with (u+ulp u)%R.
-pattern u at 3; replace u with (round beta fexp Zfloor (u + ulp u / 2)).
+apply Rnd_DN_pt_N with (succ u)%R.
+pattern u at 3; replace u with (round beta fexp Zfloor ((u + succ u) / 2)).
 apply round_DN_pt...
-apply round_DN_succ; try assumption.
+apply round_DN_eq_betw; trivial.
 split; try left; assumption.
-replace (u+ulp u)%R with (round beta fexp Zceil (u + ulp u / 2)).
+pattern (succ u) at 2; replace (succ u) with (round beta fexp Zceil ((u + succ u) / 2)).
 apply round_UP_pt...
-apply round_UP_succ; try assumption...
+apply round_UP_eq_betw; trivial.
+apply generic_format_succ...
+rewrite pred_succ; trivial.
 split; try left; assumption.
 right; field.
 Qed.
 
 
-Theorem rnd_N_ge_half_an_ulp_pred: forall choice u v,
- F u -> (0 < pred u)%R -> (u - (ulp (pred u))/2 < v)%R
+Theorem round_N_ge_midp: forall choice u v,
+ F u ->  ((u + pred u)/2 < v)%R
       -> (u <= round beta fexp (Znearest choice)  v)%R.
 Proof with auto with typeclass_instances.
-intros choice u v Fu Hu H.
-(* . *)
-assert (0 < u)%R.
-apply Rlt_trans with (1:= Hu).
-apply pred_lt_id.
-assert (0 < ulp (pred u) / 2)%R.
-unfold Rdiv; apply Rmult_lt_0_compat.
-unfold ulp; apply bpow_gt_0.
-auto with real.
-assert (ulp (pred u) / 2 < ulp (pred u))%R.
-apply Rlt_le_trans with (ulp (pred u) *1)%R;[idtac|right; ring].
-unfold Rdiv; apply Rmult_lt_compat_l.
-apply bpow_gt_0.
-apply Rmult_lt_reg_l with 2%R.
-auto with real.
-apply Rle_lt_trans with 1%R.
-right; field.
-rewrite Rmult_1_r; auto with real.
-(* *)
-apply Rnd_N_pt_monotone with F (u - ulp (pred u) / 2)%R v...
-2: apply round_N_pt...
-apply Rnd_UP_pt_N with (pred u).
-pattern (pred u) at 2; replace (pred u) with (round beta fexp Zfloor (u - ulp (pred u) / 2)).
-apply round_DN_pt...
-replace  (u - ulp (pred u) / 2)%R  with (pred u + ulp (pred u) / 2)%R.
-apply round_DN_succ; try assumption.
-apply generic_format_pred; assumption.
-split; [left|idtac]; assumption.
-pattern u at 3; rewrite <- (pred_plus_ulp u); try assumption.
-field.
-now apply Rgt_not_eq.
-pattern u at 3; replace u with (round beta fexp Zceil (u - ulp (pred u) / 2)).
-apply round_UP_pt...
-replace  (u - ulp (pred u) / 2)%R  with (pred u + ulp (pred u) / 2)%R.
-apply trans_eq with (pred u +ulp(pred u))%R.
-apply round_UP_succ; try assumption...
-apply generic_format_pred; assumption.
-split; [idtac|left]; assumption.
-apply pred_plus_ulp; try assumption.
-now apply Rgt_not_eq.
-pattern u at 3; rewrite <- (pred_plus_ulp u); try assumption.
-field.
-now apply Rgt_not_eq.
-pattern u at 4; rewrite <- (pred_plus_ulp u); try assumption.
+intros choice u v Fu H.
+rewrite <- (Ropp_involutive v).
+rewrite round_N_opp.
+rewrite <- (Ropp_involutive u).
+apply Ropp_le_contravar.
+apply round_N_le_midp.
+now apply generic_format_opp.
+apply Ropp_lt_cancel.
+rewrite Ropp_involutive.
+apply Rle_lt_trans with (2:=H).
+unfold pred.
 right; field.
-now apply Rgt_not_eq.
 Qed.
 
 
-Theorem rnd_N_ge_half_an_ulp: forall choice u v,
-  F u -> (0 < u)%R -> (u <> bpow (ln_beta beta u - 1))%R
-        -> (u - (ulp u)/2 < v)%R
-        -> (u <= round beta fexp (Znearest choice) v)%R.
+Lemma round_N_eq_DN: forall choice x,
+       let d:=round beta fexp Zfloor x in
+       let u:=round beta fexp Zceil x in
+      (x<(d+u)/2)%R ->
+     round beta fexp (Znearest choice) x = d.
 Proof with auto with typeclass_instances.
-intros choice u v Fu Hupos Hu H.
-(* *)
-assert (bpow (ln_beta beta u-1) <= pred u)%R.
-apply le_pred_lt; try assumption.
-apply generic_format_bpow.
-assert (canonic_exp beta fexp u < ln_beta beta u)%Z.
-apply ln_beta_generic_gt; try assumption.
-now apply Rgt_not_eq.
-unfold canonic_exp in H0.
-ring_simplify (ln_beta beta u - 1 + 1)%Z.
-omega.
-destruct ln_beta as (e,He); simpl in *.
-assert (bpow (e - 1) <= Rabs u)%R.
-apply He.
-now apply Rgt_not_eq.
-rewrite Rabs_right in H0.
-case H0; auto.
-intros T; contradict T.
-now apply sym_not_eq.
-apply Rle_ge; now left.
-assert (Hu2:(ulp (pred u) = ulp u)).
-unfold ulp, canonic_exp.
-apply f_equal; apply f_equal.
-apply ln_beta_unique.
-rewrite Rabs_right.
-split.
-assumption.
-apply Rlt_trans with (1:=pred_lt_id _).
-destruct ln_beta as (e,He); simpl in *.
-rewrite Rabs_right in He.
-apply He.
-now apply Rgt_not_eq.
-apply Rle_ge; now left.
-apply Rle_ge, pred_ge_0; assumption.
-apply rnd_N_ge_half_an_ulp_pred; try assumption.
-apply Rlt_le_trans with (2:=H0).
-apply bpow_gt_0.
-rewrite Hu2; assumption.
+intros choice x d u H.
+apply Rle_antisym.
+destruct (generic_format_EM beta fexp x) as [Fx|Fx].
+rewrite round_generic...
+apply round_DN_pt; trivial; now right.
+apply round_N_le_midp.
+apply round_DN_pt...
+apply Rlt_le_trans with (1:=H).
+right; apply f_equal2; trivial; apply f_equal.
+now apply sym_eq, succ_DN_eq_UP.
+apply round_ge_generic; try apply round_DN_pt...
 Qed.
 
-
-Lemma round_N_DN_betw: forall choice x d u,
-   Rnd_DN_pt (generic_format beta fexp) x d ->
-   Rnd_UP_pt (generic_format beta fexp) x u ->
-     (d<=x<(d+u)/2)%R ->
+Lemma round_N_eq_DN_pt: forall choice x d u,
+      Rnd_DN_pt F x d -> Rnd_UP_pt F x u ->
+      (x<(d+u)/2)%R ->
      round beta fexp (Znearest choice) x = d.
 Proof with auto with typeclass_instances.
 intros choice x d u Hd Hu H.
-apply Rnd_N_pt_unicity with (generic_format beta fexp) x d u; try assumption.
-intros Y.
-absurd (x < (d+u)/2)%R; try apply H.
-apply Rle_not_lt; right.
-apply Rplus_eq_reg_r with (-x)%R.
-apply trans_eq with (- (x-d)/2 + (u-x)/2)%R.
-field.
-rewrite Y; field.
-apply round_N_pt...
-apply Rnd_DN_UP_pt_N with d u...
-apply Hd.
-right; apply trans_eq with (-(d-x))%R;[idtac|ring].
-apply Rabs_left1.
-apply Rplus_le_reg_l with x; ring_simplify.
-apply H.
-rewrite Rabs_left1.
-apply Rplus_le_reg_l with (d+x)%R.
-apply Rmult_le_reg_l with (/2)%R.
-auto with real.
-apply Rle_trans with x.
-right; field.
-apply Rle_trans with ((d+u)/2)%R.
-now left.
-right; field.
-apply Rplus_le_reg_l with x; ring_simplify.
-apply H.
+assert (H0:(d = round beta fexp Zfloor x)%R).
+apply Rnd_DN_pt_unicity with (1:=Hd).
+apply round_DN_pt...
+rewrite H0.
+apply round_N_eq_DN.
+rewrite <- H0.
+rewrite Rnd_UP_pt_unicity with F x (round beta fexp Zceil x) u; try assumption.
+apply round_UP_pt...
 Qed.
 
+Lemma round_N_eq_UP: forall choice x,
+      let d:=round beta fexp Zfloor x in
+      let u:=round beta fexp Zceil x in
+     ((d+u)/2 < x)%R ->
+     round beta fexp (Znearest choice) x = u.
+Proof with auto with typeclass_instances.
+intros choice x d u H.
+apply Rle_antisym.
+apply round_le_generic; try apply round_UP_pt...
+destruct (generic_format_EM beta fexp x) as [Fx|Fx].
+rewrite round_generic...
+apply round_UP_pt; trivial; now right.
+apply round_N_ge_midp.
+apply round_UP_pt...
+apply Rle_lt_trans with (2:=H).
+right; apply f_equal2; trivial; rewrite Rplus_comm; apply f_equal2; trivial.
+now apply pred_UP_eq_DN.
+Qed.
 
-Lemma round_N_UP_betw: forall choice x d u,
-   Rnd_DN_pt (generic_format beta fexp) x d ->
-   Rnd_UP_pt (generic_format beta fexp) x u ->
-     ((d+u)/2 < x <= u)%R ->
+Lemma round_N_eq_UP_pt: forall choice x d u,
+      Rnd_DN_pt F x d -> Rnd_UP_pt F x u ->
+      ((d+u)/2 < x)%R ->
      round beta fexp (Znearest choice) x = u.
 Proof with auto with typeclass_instances.
 intros choice x d u Hd Hu H.
-rewrite <- (Ropp_involutive (round beta fexp (Znearest choice) x )),
-  <- (Ropp_involutive u) .
-apply f_equal.
-rewrite <- (Ropp_involutive x) .
-rewrite round_N_opp, Ropp_involutive.
-apply round_N_DN_betw with (-d)%R.
-replace u with (round beta fexp Zceil x).
-rewrite <- round_DN_opp.
-apply round_DN_pt...
-apply Rnd_UP_pt_unicity with (generic_format beta fexp) x...
-apply round_UP_pt...
-replace d with (round beta fexp Zfloor x).
-rewrite <- round_UP_opp.
+assert (H0:(u = round beta fexp Zceil x)%R).
+apply Rnd_UP_pt_unicity with (1:=Hu).
 apply round_UP_pt...
-apply Rnd_DN_pt_unicity with (generic_format beta fexp) x...
+rewrite H0.
+apply round_N_eq_UP.
+rewrite <- H0.
+rewrite Rnd_DN_pt_unicity with F x (round beta fexp Zfloor x) d; try assumption.
 apply round_DN_pt...
-split.
-apply Ropp_le_contravar, H.
-apply Rlt_le_trans with (-((d + u) / 2))%R.
-apply Ropp_lt_contravar, H.
-unfold Rdiv; right; ring.
 Qed.
 
-
 End Fcore_ulp.
diff --git a/flocq/Flocq_version.v b/flocq/Flocq_version.v
index d2d9d3fb..c391f590 100644
--- a/flocq/Flocq_version.v
+++ b/flocq/Flocq_version.v
@@ -25,7 +25,8 @@ Definition Flocq_version := Eval vm_compute in
   let fix parse s major minor :=
     match s with
     | String "."%char t => parse t (major * 100 + minor)%N N0
-    | String h t => parse t major (minor + N_of_ascii h - N_of_ascii "0"%char)%N
+    | String h t =>
+      parse t major (minor * 10 + N_of_ascii h - N_of_ascii "0"%char)%N
     | Empty_string => (major * 100 + minor)%N
     end in
-  parse "2.4.0"%string N0 N0.
+  parse "2.5.0"%string N0 N0.
diff --git a/flocq/Prop/Fprop_div_sqrt_error.v b/flocq/Prop/Fprop_div_sqrt_error.v
index ec00ca4e..9d29001d 100644
--- a/flocq/Prop/Fprop_div_sqrt_error.v
+++ b/flocq/Prop/Fprop_div_sqrt_error.v
@@ -95,9 +95,6 @@ intros e; apply Zle_refl.
 now rewrite F2R_opp, F2R_mult, <- Hr1, <- Hy1.
 (* *)
 destruct (relative_error_FLX_ex beta prec (prec_gt_0 prec) rnd (x / y)%R) as (eps,(Heps1,Heps2)).
-apply Rmult_integral_contrapositive_currified.
-exact Zx.
-now apply Rinv_neq_0_compat.
 rewrite Heps2.
 rewrite <- Rabs_Ropp.
 replace (-(x + - (x / y * (1 + eps) * y)))%R with (x * eps)%R by now field.
@@ -135,8 +132,11 @@ now apply Rabs_pos_lt.
 rewrite Rabs_Ropp.
 replace (bpow (Fexp fr)) with (ulp beta (FLX_exp prec) (F2R fr)).
 rewrite <- Hr1.
-apply ulp_error_f...
-unfold ulp; apply f_equal.
+apply error_lt_ulp_round...
+apply Rmult_integral_contrapositive_currified; try apply Rinv_neq_0_compat; assumption.
+rewrite ulp_neq_0.
+2: now rewrite <- Hr1.
+apply f_equal.
 now rewrite Hr2, <- Hr1.
 replace (prec+(Fexp fr+Fexp fy))%Z with ((prec+Fexp fy)+Fexp fr)%Z by ring.
 rewrite bpow_plus.
@@ -246,8 +246,10 @@ apply Rmult_le_compat_r.
 apply Rabs_pos.
 apply Rle_trans with (/2*ulp beta  (FLX_exp prec) (F2R fr))%R.
 rewrite <- Hr1.
-apply ulp_half_error_f...
-right; unfold ulp; apply f_equal.
+apply error_le_half_ulp_round...
+right; rewrite ulp_neq_0.
+2: now rewrite <- Hr1.
+apply f_equal.
 rewrite Hr2, <- Hr1; trivial.
 rewrite Rmult_assoc, Rmult_comm.
 replace (prec+(Fexp fr+Fexp fr))%Z with (Fexp fr + (prec+Fexp fr))%Z by ring.
diff --git a/flocq/Prop/Fprop_mult_error.v b/flocq/Prop/Fprop_mult_error.v
index e84e80b4..7c71627b 100644
--- a/flocq/Prop/Fprop_mult_error.v
+++ b/flocq/Prop/Fprop_mult_error.v
@@ -126,8 +126,9 @@ apply Zplus_le_compat_r.
 rewrite ln_beta_unique with (1 := Hexy).
 apply ln_beta_le_bpow with (1 := Hz).
 replace (bpow (exy - prec)) with (ulp beta (FLX_exp prec) (x * y)).
-apply ulp_error...
-unfold ulp, canonic_exp.
+apply error_lt_ulp...
+rewrite ulp_neq_0; trivial.
+unfold canonic_exp.
 now rewrite ln_beta_unique with (1 := Hexy).
 apply Hc1.
 reflexivity.
diff --git a/flocq/Prop/Fprop_relative.v b/flocq/Prop/Fprop_relative.v
index f0a8f344..585b71da 100644
--- a/flocq/Prop/Fprop_relative.v
+++ b/flocq/Prop/Fprop_relative.v
@@ -35,7 +35,7 @@ Section relative_error_conversion.
 Variable rnd : R -> Z.
 Context { valid_rnd : Valid_rnd rnd }.
 
-Lemma relative_error_lt_conversion' :
+Lemma relative_error_lt_conversion :
   forall x b, (0 < b)%R ->
   (x <> 0 -> Rabs (round beta fexp rnd x - x) < b * Rabs x)%R ->
   exists eps,
@@ -62,19 +62,6 @@ rewrite Rinv_l with (1 := Hx0).
 now rewrite Rabs_R1, Rmult_1_r.
 Qed.
 
-(* TODO: remove *)
-Lemma relative_error_lt_conversion :
-  forall x b, (0 < b)%R ->
-  (Rabs (round beta fexp rnd x - x) < b * Rabs x)%R ->
-  exists eps,
-  (Rabs eps < b)%R /\ round beta fexp rnd x = (x * (1 + eps))%R.
-Proof.
-intros x b Hb0 Hxb.
-apply relative_error_lt_conversion'.
-exact Hb0.
-now intros _.
-Qed.
-
 Lemma relative_error_le_conversion :
   forall x b, (0 <= b)%R ->
   (Rabs (round beta fexp rnd x - x) <= b * Rabs x)%R ->
@@ -113,16 +100,15 @@ Theorem relative_error :
   forall x,
   (bpow emin <= Rabs x)%R ->
   (Rabs (round beta fexp rnd x - x) < bpow (-p + 1) * Rabs x)%R.
-Proof.
+Proof with auto with typeclass_instances.
 intros x Hx.
-apply Rlt_le_trans with (ulp beta fexp x)%R.
-now apply ulp_error.
-unfold ulp, canonic_exp.
 assert (Hx': (x <> 0)%R).
-intros H.
-apply Rlt_not_le with (2 := Hx).
-rewrite H, Rabs_R0.
-apply bpow_gt_0.
+intros T; contradict Hx; rewrite T, Rabs_R0.
+apply Rlt_not_le, bpow_gt_0.
+apply Rlt_le_trans with (ulp beta fexp x)%R.
+now apply error_lt_ulp...
+rewrite ulp_neq_0; trivial.
+unfold canonic_exp.
 destruct (ln_beta beta x) as (ex, He).
 simpl.
 specialize (He Hx').
@@ -150,6 +136,7 @@ Proof with auto with typeclass_instances.
 intros x Hx.
 apply relative_error_lt_conversion...
 apply bpow_gt_0.
+intros _.
 now apply relative_error.
 Qed.
 
@@ -168,28 +155,17 @@ rewrite F2R_0, F2R_Zabs.
 now apply Rabs_pos_lt.
 Qed.
 
-Theorem relative_error_F2R_emin_ex' :
+Theorem relative_error_F2R_emin_ex :
   forall m, let x := F2R (Float beta m emin) in
   exists eps,
   (Rabs eps < bpow (-p + 1))%R /\ round beta fexp rnd x = (x * (1 + eps))%R.
 Proof with auto with typeclass_instances.
 intros m x.
-apply relative_error_lt_conversion'...
+apply relative_error_lt_conversion...
 apply bpow_gt_0.
 now apply relative_error_F2R_emin.
 Qed.
 
-(* TODO: remove *)
-Theorem relative_error_F2R_emin_ex :
-  forall m, let x := F2R (Float beta m emin) in
-  (x <> 0)%R ->
-  exists eps,
-  (Rabs eps < bpow (-p + 1))%R /\ round beta fexp rnd x = (x * (1 + eps))%R.
-Proof with auto with typeclass_instances.
-intros m x _.
-apply relative_error_F2R_emin_ex'.
-Qed.
-
 Theorem relative_error_round :
   (0 < p)%Z ->
   forall x,
@@ -197,14 +173,13 @@ Theorem relative_error_round :
   (Rabs (round beta fexp rnd x - x) < bpow (-p + 1) * Rabs (round beta fexp rnd x))%R.
 Proof with auto with typeclass_instances.
 intros Hp x Hx.
-apply Rlt_le_trans with (ulp beta fexp x)%R.
-now apply ulp_error.
 assert (Hx': (x <> 0)%R).
-intros H.
-apply Rlt_not_le with (2 := Hx).
-rewrite H, Rabs_R0.
-apply bpow_gt_0.
-unfold ulp, canonic_exp.
+intros T; contradict Hx; rewrite T, Rabs_R0.
+apply Rlt_not_le, bpow_gt_0.
+apply Rlt_le_trans with (ulp beta fexp x)%R.
+now apply error_lt_ulp.
+rewrite ulp_neq_0; trivial.
+unfold canonic_exp.
 destruct (ln_beta beta x) as (ex, He).
 simpl.
 specialize (He Hx').
@@ -222,7 +197,7 @@ apply bpow_ge_0.
 generalize He.
 apply round_abs_abs...
 clear rnd valid_rnd x Hx Hx' He.
-intros rnd valid_rnd x Hx.
+intros rnd valid_rnd x _ Hx.
 rewrite <- (round_generic beta fexp rnd (bpow (ex - 1))).
 now apply round_le.
 apply generic_format_bpow.
@@ -257,7 +232,7 @@ Theorem relative_error_N :
 Proof.
 intros x Hx.
 apply Rle_trans with (/2 * ulp beta fexp x)%R.
-now apply ulp_half_error.
+now apply error_le_half_ulp.
 rewrite Rmult_assoc.
 apply Rmult_le_compat_l.
 apply Rlt_le.
@@ -268,7 +243,8 @@ intros H.
 apply Rlt_not_le with (2 := Hx).
 rewrite H, Rabs_R0.
 apply bpow_gt_0.
-unfold ulp, canonic_exp.
+rewrite ulp_neq_0; trivial.
+unfold canonic_exp.
 destruct (ln_beta beta x) as (ex, He).
 simpl.
 specialize (He Hx').
@@ -348,7 +324,7 @@ Theorem relative_error_N_round :
 Proof with auto with typeclass_instances.
 intros Hp x Hx.
 apply Rle_trans with (/2 * ulp beta fexp x)%R.
-now apply ulp_half_error.
+now apply error_le_half_ulp.
 rewrite Rmult_assoc.
 apply Rmult_le_compat_l.
 apply Rlt_le.
@@ -359,7 +335,8 @@ intros H.
 apply Rlt_not_le with (2 := Hx).
 rewrite H, Rabs_R0.
 apply bpow_gt_0.
-unfold ulp, canonic_exp.
+rewrite ulp_neq_0; trivial.
+unfold canonic_exp.
 destruct (ln_beta beta x) as (ex, He).
 simpl.
 specialize (He Hx').
@@ -377,7 +354,7 @@ apply bpow_ge_0.
 generalize He.
 apply round_abs_abs...
 clear rnd valid_rnd x Hx Hx' He.
-intros rnd valid_rnd x Hx.
+intros rnd valid_rnd x _ Hx.
 rewrite <- (round_generic beta fexp rnd (bpow (ex - 1))).
 now apply round_le.
 apply generic_format_bpow.
@@ -428,17 +405,6 @@ Qed.
 Variable rnd : R -> Z.
 Context { valid_rnd : Valid_rnd rnd }.
 
-(* TODO: remove *)
-Theorem relative_error_FLT_F2R_emin :
-  forall m, let x := F2R (Float beta m (emin + prec - 1)) in
-  (x <> 0)%R ->
-  (Rabs (round beta (FLT_exp emin prec) rnd x - x) < bpow (-prec + 1) * Rabs x)%R.
-Proof with auto with typeclass_instances.
-intros m x Hx.
-apply relative_error_F2R_emin...
-apply relative_error_FLT_aux.
-Qed.
-
 Theorem relative_error_FLT :
   forall x,
   (bpow (emin + prec - 1) <= Rabs x)%R ->
@@ -449,7 +415,7 @@ apply relative_error with (emin + prec - 1)%Z...
 apply relative_error_FLT_aux.
 Qed.
 
-Theorem relative_error_FLT_F2R_emin' :
+Theorem relative_error_FLT_F2R_emin :
   forall m, let x := F2R (Float beta m emin) in
   (x <> 0)%R ->
   (Rabs (round beta (FLT_exp emin prec) rnd x - x) < bpow (-prec + 1) * Rabs x)%R.
@@ -472,26 +438,13 @@ now exists (Float beta m emin).
 now apply relative_error_FLT.
 Qed.
 
-Theorem relative_error_FLT_F2R_emin_ex' :
+Theorem relative_error_FLT_F2R_emin_ex :
   forall m, let x := F2R (Float beta m emin) in
   exists eps,
   (Rabs eps < bpow (-prec + 1))%R /\ round beta (FLT_exp emin prec) rnd x = (x * (1 + eps))%R.
 Proof with auto with typeclass_instances.
 intros m x.
-apply relative_error_lt_conversion'...
-apply bpow_gt_0.
-now apply relative_error_FLT_F2R_emin'.
-Qed.
-
-(* TODO: remove *)
-Theorem relative_error_FLT_F2R_emin_ex :
-  forall m, let x := F2R (Float beta m (emin + prec - 1)) in
-  (x <> 0)%R ->
-  exists eps,
-  (Rabs eps < bpow (-prec + 1))%R /\ round beta (FLT_exp emin prec) rnd x = (x * (1 + eps))%R.
-Proof with auto with typeclass_instances.
-intros m x _.
-apply relative_error_lt_conversion'...
+apply relative_error_lt_conversion...
 apply bpow_gt_0.
 now apply relative_error_FLT_F2R_emin.
 Qed.
@@ -506,7 +459,7 @@ Proof with auto with typeclass_instances.
 intros x Hx.
 apply relative_error_lt_conversion...
 apply bpow_gt_0.
-now apply relative_error_FLT.
+intros _; now apply relative_error_FLT.
 Qed.
 
 Variable choice : Z -> bool.
@@ -548,7 +501,7 @@ apply relative_error_N_round with (emin + prec - 1)%Z...
 apply relative_error_FLT_aux.
 Qed.
 
-Theorem relative_error_N_FLT_F2R_emin' :
+Theorem relative_error_N_FLT_F2R_emin :
   forall m, let x := F2R (Float beta m emin) in
   (Rabs (round beta (FLT_exp emin prec) (Znearest choice) x - x) <= /2 * bpow (-prec + 1) * Rabs x)%R.
 Proof with auto with typeclass_instances.
@@ -573,17 +526,7 @@ now exists (Float beta m emin).
 now apply relative_error_N_FLT.
 Qed.
 
-(* TODO: remove *)
-Theorem relative_error_N_FLT_F2R_emin :
-  forall m, let x := F2R (Float beta m (emin + prec - 1)) in
-  (Rabs (round beta (FLT_exp emin prec) (Znearest choice) x - x) <= /2 * bpow (-prec + 1) * Rabs x)%R.
-Proof with auto with typeclass_instances.
-intros m x.
-apply relative_error_N_F2R_emin...
-apply relative_error_FLT_aux.
-Qed.
-
-Theorem relative_error_N_FLT_F2R_emin_ex' :
+Theorem relative_error_N_FLT_F2R_emin_ex :
   forall m, let x := F2R (Float beta m emin) in
   exists eps,
   (Rabs eps <= /2 * bpow (-prec + 1))%R /\ round beta (FLT_exp emin prec) (Znearest choice) x = (x * (1 + eps))%R.
@@ -594,26 +537,11 @@ apply Rmult_le_pos.
 apply Rlt_le.
 apply (RinvN_pos 1).
 apply bpow_ge_0.
-now apply relative_error_N_FLT_F2R_emin'.
-Qed.
-
-(* TODO: remove *)
-Theorem relative_error_N_FLT_F2R_emin_ex :
-  forall m, let x := F2R (Float beta m (emin + prec - 1)) in
-  exists eps,
-  (Rabs eps <= /2 * bpow (-prec + 1))%R /\ round beta (FLT_exp emin prec) (Znearest choice) x = (x * (1 + eps))%R.
-Proof with auto with typeclass_instances.
-intros m x.
-apply relative_error_le_conversion...
-apply Rlt_le.
-apply Rmult_lt_0_compat.
-apply Rinv_0_lt_compat.
-now apply (Z2R_lt 0 2).
-apply bpow_gt_0.
 now apply relative_error_N_FLT_F2R_emin.
 Qed.
 
-Theorem relative_error_N_FLT_round_F2R_emin' :
+
+Theorem relative_error_N_FLT_round_F2R_emin :
   forall m, let x := F2R (Float beta m emin) in
   (Rabs (round beta (FLT_exp emin prec) (Znearest choice) x - x) <= /2 * bpow (-prec + 1) * Rabs (round beta (FLT_exp emin prec) (Znearest choice) x))%R.
 Proof with auto with typeclass_instances.
@@ -639,16 +567,6 @@ apply relative_error_N_round with (emin := (emin + prec - 1)%Z)...
 apply relative_error_FLT_aux.
 Qed.
 
-(* TODO: remove *)
-Theorem relative_error_N_FLT_round_F2R_emin :
-  forall m, let x := F2R (Float beta m (emin + prec - 1)) in
-  (Rabs (round beta (FLT_exp emin prec) (Znearest choice) x - x) <= /2 * bpow (-prec + 1) * Rabs (round beta (FLT_exp emin prec) (Znearest choice) x))%R.
-Proof with auto with typeclass_instances.
-intros m x.
-apply relative_error_N_round_F2R_emin...
-apply relative_error_FLT_aux.
-Qed.
-
 Lemma error_N_FLT_aux :
   forall x,
   (0 < x)%R ->
@@ -682,10 +600,11 @@ auto with real.
 apply bpow_ge_0.
 split.
 apply Rle_trans with (/2*ulp beta (FLT_exp emin prec) x)%R.
-apply ulp_half_error.
+apply error_le_half_ulp.
 now apply FLT_exp_valid.
 apply Rmult_le_compat_l; auto with real.
-unfold ulp.
+rewrite ulp_neq_0.
+2: now apply Rgt_not_eq.
 apply bpow_le.
 unfold FLT_exp, canonic_exp.
 rewrite Zmax_right.
@@ -770,28 +689,17 @@ apply He.
 Qed.
 
 (** 1+#&epsilon;# property in any rounding in FLX *)
-Theorem relative_error_FLX_ex' :
+Theorem relative_error_FLX_ex :
   forall x,
   exists eps,
   (Rabs eps < bpow (-prec + 1))%R /\ round beta (FLX_exp prec) rnd x = (x * (1 + eps))%R.
 Proof with auto with typeclass_instances.
 intros x.
-apply relative_error_lt_conversion'...
+apply relative_error_lt_conversion...
 apply bpow_gt_0.
 now apply relative_error_FLX.
 Qed.
 
-(* TODO: remove *)
-Theorem relative_error_FLX_ex :
-  forall x,
-  (x <> 0)%R ->
-  exists eps,
-  (Rabs eps < bpow (-prec + 1))%R /\ round beta (FLX_exp prec) rnd x = (x * (1 + eps))%R.
-Proof with auto with typeclass_instances.
-intros x _.
-apply relative_error_FLX_ex'.
-Qed.
-
 Theorem relative_error_FLX_round :
   forall x,
   (x <> 0)%R ->