Upgrade to flocq 2.4.0

6 files changed, 942 insertions, 98 deletions

diff --git a/flocq/Core/Fcore_FLT.v b/flocq/Core/Fcore_FLT.v
index c057b6ce..273ff69f 100644
--- a/flocq/Core/Fcore_FLT.v
+++ b/flocq/Core/Fcore_FLT.v
@@ -104,6 +104,19 @@ apply Zle_max_l.
 apply Zle_max_r.
 Qed.
 
+
+Theorem FLT_format_bpow :
+  forall e, (emin <= e)%Z -> generic_format beta FLT_exp (bpow e).
+Proof.
+intros e He.
+apply generic_format_bpow; unfold FLT_exp.
+apply Z.max_case; try assumption.
+unfold Prec_gt_0 in prec_gt_0_; omega.
+Qed.
+
+
+
+
 Theorem FLT_format_satisfies_any :
   satisfies_any FLT_format.
 Proof.
@@ -115,11 +128,14 @@ apply generic_format_FLT.
 Qed.
 
 Theorem canonic_exp_FLT_FLX :
-  forall x, x <> R0 ->
+  forall x,
   (bpow (emin + prec - 1) <= Rabs x)%R ->
   canonic_exp beta FLT_exp x = canonic_exp beta (FLX_exp prec) x.
 Proof.
-intros x Hx0 Hx.
+intros x Hx.
+assert (Hx0: x <> 0%R).
+intros H1; rewrite H1, Rabs_R0 in Hx.
+contradict Hx; apply Rlt_not_le, bpow_gt_0.
 unfold canonic_exp.
 apply Zmax_left.
 destruct (ln_beta beta x) as (ex, He).
@@ -166,10 +182,6 @@ Theorem round_FLT_FLX : forall rnd x,
 intros rnd x Hx.
 unfold round, scaled_mantissa.
 rewrite canonic_exp_FLT_FLX ; trivial.
-contradict Hx.
-rewrite Hx, Rabs_R0.
-apply Rlt_not_le.
-apply bpow_gt_0.
 Qed.
 
 (** Links between FLT and FIX (underflow) *)
diff --git a/flocq/Core/Fcore_Raux.v b/flocq/Core/Fcore_Raux.v
index d8110198..3758324f 100644
--- a/flocq/Core/Fcore_Raux.v
+++ b/flocq/Core/Fcore_Raux.v
@@ -73,6 +73,24 @@ apply Rplus_eq_reg_l with r.
 now rewrite 2!(Rplus_comm r).
 Qed.
 
+Theorem Rplus_lt_reg_l :
+  forall r r1 r2 : R,
+  (r + r1 < r + r2)%R -> (r1 < r2)%R.
+Proof.
+intros.
+solve [ apply Rplus_lt_reg_l with (1 := H) |
+        apply Rplus_lt_reg_r with (1 := H) ].
+Qed.
+
+Theorem Rplus_lt_reg_r :
+  forall r r1 r2 : R,
+  (r1 + r < r2 + r)%R -> (r1 < r2)%R.
+Proof.
+intros.
+apply Rplus_lt_reg_l with r.
+now rewrite 2!(Rplus_comm r).
+Qed.
+
 Theorem Rplus_le_reg_r :
   forall r r1 r2 : R,
   (r1 + r <= r2 + r)%R -> (r1 <= r2)%R.
@@ -102,6 +120,21 @@ exact H.
 now rewrite 2!(Rmult_comm r).
 Qed.
 
+Theorem Rmult_lt_compat :
+  forall r1 r2 r3 r4,
+  (0 <= r1)%R -> (0 <= r3)%R -> (r1 < r2)%R -> (r3 < r4)%R ->
+  (r1 * r3 < r2 * r4)%R.
+Proof.
+intros r1 r2 r3 r4 Pr1 Pr3 H12 H34.
+apply Rle_lt_trans with (r1 * r4)%R.
+- apply Rmult_le_compat_l.
+  + exact Pr1.
+  + now apply Rlt_le.
+- apply Rmult_lt_compat_r.
+  + now apply Rle_lt_trans with r3.
+  + exact H12.
+Qed.
+
 Theorem Rmult_eq_reg_r :
   forall r r1 r2 : R, (r1 * r)%R = (r2 * r)%R ->
   r <> 0%R -> r1 = r2.
@@ -219,6 +252,21 @@ apply Rle_refl.
 apply Rsqrt_positivity.
 Qed.
 
+Lemma sqrt_neg : forall x, (x <= 0)%R -> (sqrt x = 0)%R.
+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.
+
 Theorem Rabs_le :
   forall x y,
   (-y <= x <= y)%R -> (Rabs x <= y)%R.
@@ -1768,6 +1816,25 @@ now apply Rlt_le.
 now apply Rlt_le.
 Qed.
 
+Lemma ln_beta_lt_pos :
+  forall x y,
+  (0 < x)%R -> (0 < y)%R ->
+  (ln_beta x < ln_beta y)%Z -> (x < y)%R.
+Proof.
+intros x y Px Py.
+destruct (ln_beta x) as (ex, Hex).
+destruct (ln_beta y) as (ey, Hey).
+simpl.
+intro H.
+destruct Hex as (_,Hex); [now apply Rgt_not_eq|].
+destruct Hey as (Hey,_); [now apply Rgt_not_eq|].
+rewrite Rabs_right in Hex; [|now apply Rle_ge; apply Rlt_le].
+rewrite Rabs_right in Hey; [|now apply Rle_ge; apply Rlt_le].
+apply (Rlt_le_trans _ _ _ Hex).
+apply Rle_trans with (bpow (ey - 1)); [|exact Hey].
+now apply bpow_le; omega.
+Qed.
+
 Theorem ln_beta_bpow :
   forall e, (ln_beta (bpow e) = e + 1 :> Z)%Z.
 Proof.
@@ -1834,6 +1901,23 @@ rewrite Zx, Rabs_R0.
 apply bpow_gt_0.
 Qed.
 
+Theorem ln_beta_ge_bpow :
+  forall x e,
+  (bpow (e - 1) <= Rabs x)%R ->
+  (e <= ln_beta x)%Z.
+Proof.
+intros x e H.
+destruct (Rlt_or_le (Rabs x) (bpow e)) as [Hxe|Hxe].
+- (* Rabs x w bpow e *)
+  assert (ln_beta x = e :> Z) as Hln.
+  now apply ln_beta_unique; split.
+  rewrite Hln.
+  now apply Z.le_refl.
+- (* bpow e <= Rabs x *)
+  apply Zlt_le_weak.
+  now apply ln_beta_gt_bpow.
+Qed.
+
 Theorem bpow_ln_beta_gt :
   forall x,
   (Rabs x < bpow (ln_beta x))%R.
@@ -1885,6 +1969,221 @@ clear -Zm.
 zify ; omega.
 Qed.
 
+Lemma ln_beta_mult :
+  forall x y,
+  (x <> 0)%R -> (y <> 0)%R ->
+  (ln_beta x + ln_beta y - 1 <= ln_beta (x * y) <= ln_beta x + ln_beta y)%Z.
+Proof.
+intros x y Hx Hy.
+destruct (ln_beta x) as (ex, Hx2).
+destruct (ln_beta y) as (ey, Hy2).
+simpl.
+destruct (Hx2 Hx) as (Hx21,Hx22); clear Hx2.
+destruct (Hy2 Hy) as (Hy21,Hy22); clear Hy2.
+assert (Hxy : (bpow (ex + ey - 1 - 1) <= Rabs (x * y))%R).
+{ replace (ex + ey -1 -1)%Z with (ex - 1 + (ey - 1))%Z; [|ring].
+  rewrite bpow_plus.
+  rewrite Rabs_mult.
+  now apply Rmult_le_compat; try apply bpow_ge_0. }
+assert (Hxy2 : (Rabs (x * y) < bpow (ex + ey))%R).
+{ rewrite Rabs_mult.
+  rewrite bpow_plus.
+  apply Rmult_le_0_lt_compat; try assumption.
+  now apply Rle_trans with (bpow (ex - 1)); try apply bpow_ge_0.
+  now apply Rle_trans with (bpow (ey - 1)); try apply bpow_ge_0. }
+split.
+- now apply ln_beta_ge_bpow.
+- apply ln_beta_le_bpow.
+  + now apply Rmult_integral_contrapositive_currified.
+  + assumption.
+Qed.
+
+Lemma ln_beta_plus :
+  forall x y,
+  (0 < y)%R -> (y <= x)%R ->
+  (ln_beta x <= ln_beta (x + y) <= ln_beta x + 1)%Z.
+Proof.
+assert (Hr : (2 <= r)%Z).
+{ destruct r as (beta_val,beta_prop).
+  now apply Zle_bool_imp_le. }
+intros x y Hy Hxy.
+assert (Hx : (0 < x)%R) by apply (Rlt_le_trans _ _ _ Hy Hxy).
+destruct (ln_beta x) as (ex,Hex); simpl.
+destruct Hex as (Hex0,Hex1); [now apply Rgt_not_eq|].
+assert (Haxy : (Rabs (x + y) < bpow (ex + 1))%R).
+{ rewrite bpow_plus1.
+  apply Rlt_le_trans with (2 * bpow ex)%R.
+  - apply Rle_lt_trans with (2 * Rabs x)%R.
+    + rewrite Rabs_right.
+      { apply Rle_trans with (x + x)%R; [now apply Rplus_le_compat_l|].
+        rewrite Rabs_right.
+        { rewrite Rmult_plus_distr_r.
+          rewrite Rmult_1_l.
+          now apply Rle_refl. }
+        now apply Rgt_ge. }
+      apply Rgt_ge.
+      rewrite <- (Rplus_0_l 0).
+      now apply Rplus_gt_compat.
+    + now apply Rmult_lt_compat_l; intuition.
+  - apply Rmult_le_compat_r; [now apply bpow_ge_0|].
+    now change 2%R with (Z2R 2); apply Z2R_le. }
+assert (Haxy2 : (bpow (ex - 1) <= Rabs (x + y))%R).
+{ apply (Rle_trans _ _ _ Hex0).
+  rewrite Rabs_right; [|now apply Rgt_ge].
+  apply Rabs_ge; right.
+  rewrite <- (Rplus_0_r x) at 1.
+  apply Rplus_le_compat_l.
+  now apply Rlt_le. }
+split.
+- now apply ln_beta_ge_bpow.
+- apply ln_beta_le_bpow.
+  + now apply tech_Rplus; [apply Rlt_le|].
+  + exact Haxy.
+Qed.
+
+Lemma ln_beta_minus :
+  forall x y,
+  (0 < y)%R -> (y < x)%R ->
+  (ln_beta (x - y) <= ln_beta x)%Z.
+Proof.
+intros x y Py Hxy.
+assert (Px : (0 < x)%R) by apply (Rlt_trans _ _ _ Py Hxy).
+apply ln_beta_le.
+- now apply Rlt_Rminus.
+- rewrite <- (Rplus_0_r x) at 2.
+  apply Rplus_le_compat_l.
+  rewrite <- Ropp_0.
+  now apply Ropp_le_contravar; apply Rlt_le.
+Qed.
+
+Lemma ln_beta_minus_lb :
+  forall x y,
+  (0 < x)%R -> (0 < y)%R ->
+  (ln_beta y <= ln_beta x - 2)%Z ->
+  (ln_beta x - 1 <= ln_beta (x - y))%Z.
+Proof.
+assert (Hbeta : (2 <= r)%Z).
+{ destruct r as (beta_val,beta_prop).
+  now apply Zle_bool_imp_le. }
+intros x y Px Py Hln.
+assert (Oxy : (y < x)%R); [now apply ln_beta_lt_pos; [| |omega]|].
+destruct (ln_beta x) as (ex,Hex).
+destruct (ln_beta y) as (ey,Hey).
+simpl in Hln |- *.
+destruct Hex as (Hex,_); [now apply Rgt_not_eq|].
+destruct Hey as (_,Hey); [now apply Rgt_not_eq|].
+assert (Hbx : (bpow (ex - 2) + bpow (ex - 2) <= x)%R).
+{ ring_simplify.
+  apply Rle_trans with (bpow (ex - 1)).
+  - replace (ex - 1)%Z with (ex - 2 + 1)%Z by ring.
+    rewrite bpow_plus1.
+    apply Rmult_le_compat_r; [now apply bpow_ge_0|].
+    now change 2%R with (Z2R 2); apply Z2R_le.
+  - now rewrite Rabs_right in Hex; [|apply Rle_ge; apply Rlt_le]. }
+assert (Hby : (y < bpow (ex - 2))%R).
+{ apply Rlt_le_trans with (bpow ey).
+  now rewrite Rabs_right in Hey; [|apply Rle_ge; apply Rlt_le].
+  now apply bpow_le. }
+assert (Hbxy : (bpow (ex - 2) <= x - y)%R).
+{ apply Ropp_lt_contravar in Hby.
+  apply Rlt_le in Hby.
+  replace (bpow (ex - 2))%R with (bpow (ex - 2) + bpow (ex - 2)
+                                                  - bpow (ex - 2))%R by ring.
+  now apply Rplus_le_compat. }
+apply ln_beta_ge_bpow.
+replace (ex - 1 - 1)%Z with (ex - 2)%Z by ring.
+now apply Rabs_ge; right.
+Qed.
+
+Lemma ln_beta_div :
+  forall x y : R,
+  (0 < x)%R -> (0 < y)%R ->
+  (ln_beta x - ln_beta y <= ln_beta (x / y) <= ln_beta x - ln_beta y + 1)%Z.
+Proof.
+intros x y Px Py.
+destruct (ln_beta x) as (ex,Hex).
+destruct (ln_beta y) as (ey,Hey).
+simpl.
+unfold Rdiv.
+rewrite Rabs_right in Hex; [|now apply Rle_ge; apply Rlt_le].
+rewrite Rabs_right in Hey; [|now apply Rle_ge; apply Rlt_le].
+assert (Heiy : (bpow (- ey) < / y <= bpow (- ey + 1))%R).
+{ split.
+  - rewrite bpow_opp.
+    apply Rinv_lt_contravar.
+    + apply Rmult_lt_0_compat; [exact Py|].
+      now apply bpow_gt_0.
+    + apply Hey.
+      now apply Rgt_not_eq.
+  - replace (_ + _)%Z with (- (ey - 1))%Z by ring.
+    rewrite bpow_opp.
+    apply Rinv_le; [now apply bpow_gt_0|].
+    apply Hey.
+    now apply Rgt_not_eq. }
+split.
+- apply ln_beta_ge_bpow.
+  apply Rabs_ge; right.
+  replace (_ - _)%Z with (ex - 1 - ey)%Z by ring.
+  unfold Zminus at 1; rewrite bpow_plus.
+  apply Rmult_le_compat.
+  + now apply bpow_ge_0.
+  + now apply bpow_ge_0.
+  + apply Hex.
+    now apply Rgt_not_eq.
+  + apply Rlt_le; apply Heiy.
+- assert (Pxy : (0 < x * / y)%R).
+  { apply Rmult_lt_0_compat; [exact Px|].
+    now apply Rinv_0_lt_compat. }
+  apply ln_beta_le_bpow.
+  + now apply Rgt_not_eq.
+  + rewrite Rabs_right; [|now apply Rle_ge; apply Rlt_le].
+    replace (_ + 1)%Z with (ex + (- ey + 1))%Z by ring.
+    rewrite bpow_plus.
+    apply Rlt_le_trans with (bpow ex * / y)%R.
+    * apply Rmult_lt_compat_r; [now apply Rinv_0_lt_compat|].
+      apply Hex.
+      now apply Rgt_not_eq.
+    * apply Rmult_le_compat_l; [now apply bpow_ge_0|].
+      apply Heiy.
+Qed.
+
+Lemma ln_beta_sqrt :
+  forall x,
+  (0 < x)%R ->
+  (2 * ln_beta (sqrt x) - 1 <= ln_beta x <= 2 * ln_beta (sqrt x))%Z.
+Proof.
+intros x Px.
+assert (H : (bpow (2 * ln_beta (sqrt x) - 1 - 1) <= Rabs x
+            < bpow (2 * ln_beta (sqrt x)))%R).
+{ split.
+  - apply Rge_le; rewrite <- (sqrt_def x) at 1;
+    [|now apply Rlt_le]; apply Rle_ge.
+    rewrite Rabs_mult.
+    replace (_ - _)%Z with (ln_beta (sqrt x) - 1
+                            + (ln_beta (sqrt x) - 1))%Z by ring.
+    rewrite bpow_plus.
+    assert (H : (bpow (ln_beta (sqrt x) - 1) <= Rabs (sqrt x))%R).
+    { destruct (ln_beta (sqrt x)) as (esx,Hesx); simpl.
+      apply Hesx.
+      apply Rgt_not_eq; apply Rlt_gt.
+      now apply sqrt_lt_R0. }
+    now apply Rmult_le_compat; [now apply bpow_ge_0|now apply bpow_ge_0| |].
+  - rewrite <- (sqrt_def x) at 1; [|now apply Rlt_le].
+    rewrite Rabs_mult.
+    change 2%Z with (1 + 1)%Z; rewrite Zmult_plus_distr_l;
+    rewrite Zmult_1_l.
+    rewrite bpow_plus.
+    assert (H : (Rabs (sqrt x) < bpow (ln_beta (sqrt x)))%R).
+    { destruct (ln_beta (sqrt x)) as (esx,Hesx); simpl.
+      apply Hesx.
+      apply Rgt_not_eq; apply Rlt_gt.
+      now apply sqrt_lt_R0. }
+    now apply Rmult_lt_compat; [now apply Rabs_pos|now apply Rabs_pos| |]. }
+split.
+- now apply ln_beta_ge_bpow.
+- now apply ln_beta_le_bpow; [now apply Rgt_not_eq|].
+Qed.
+
 End pow.
 
 Section Bool.
@@ -2006,3 +2305,30 @@ apply refl_equal.
 Qed.
 
 End cond_Ropp.
+
+(** A little tactic to simplify terms of the form [bpow a * bpow b]. *)
+Ltac bpow_simplify :=
+  (* bpow ex * bpow ey ~~> bpow (ex + ey) *)
+  repeat
+    match goal with
+      | |- context [(bpow _ _ * bpow _ _)] =>
+        rewrite <- bpow_plus
+      | |- context [(?X1 * bpow _ _ * bpow _ _)] =>
+        rewrite (Rmult_assoc X1); rewrite <- bpow_plus
+      | |- context [(?X1 * (?X2 * bpow _ _) * bpow _ _)] =>
+        rewrite <- (Rmult_assoc X1 X2); rewrite (Rmult_assoc (X1 * X2));
+        rewrite <- bpow_plus
+    end;
+  (* ring_simplify arguments of bpow *)
+  repeat
+    match goal with
+      | |- context [(bpow _ ?X)] =>
+        progress ring_simplify X
+    end;
+  (* bpow 0 ~~> 1 *)
+  change (bpow _ 0) with 1;
+  repeat
+    match goal with
+      | |- context [(_ * 1)] =>
+        rewrite Rmult_1_r
+    end.
diff --git a/flocq/Core/Fcore_Zaux.v b/flocq/Core/Fcore_Zaux.v
index 7ba28ca4..4702d62e 100644
--- a/flocq/Core/Fcore_Zaux.v
+++ b/flocq/Core/Fcore_Zaux.v
@@ -18,7 +18,7 @@ COPYING file for more details.
 *)
 
 Require Import ZArith.
-Require Import ZOdiv.
+Require Import Zquot.
 
 Section Zmissing.
 
@@ -233,6 +233,8 @@ apply f_equal.
 apply eqbool_irrelevance.
 Qed.
 
+Definition radix2 := Build_radix 2 (refl_equal _).
+
 Variable r : radix.
 
 Theorem radix_gt_0 : (0 < r)%Z.
@@ -385,26 +387,26 @@ Qed.
 
 Theorem ZOmod_eq :
   forall a b,
-  ZOmod a b = (a - ZOdiv a b * b)%Z.
+  Z.rem a b = (a - Z.quot a b * b)%Z.
 Proof.
 intros a b.
-rewrite (ZO_div_mod_eq a b) at 2.
+rewrite (Z.quot_rem' a b) at 2.
 ring.
 Qed.
 
 Theorem ZOmod_mod_mult :
   forall n a b,
-  ZOmod (ZOmod n (a * b)) b = ZOmod n b.
+  Z.rem (Z.rem n (a * b)) b = Z.rem n b.
 Proof.
 intros n a b.
-assert (ZOmod n (a * b) = n + - (ZOdiv n (a * b) * a) * b)%Z.
+assert (Z.rem n (a * b) = n + - (Z.quot n (a * b) * a) * b)%Z.
 rewrite <- Zopp_mult_distr_l.
 rewrite <- Zmult_assoc.
 apply ZOmod_eq.
 rewrite H.
-apply ZO_mod_plus.
+apply Z_rem_plus.
 rewrite <- H.
-apply ZOmod_sgn2.
+apply Zrem_sgn2.
 Qed.
 
 Theorem Zdiv_mod_mult :
@@ -434,73 +436,73 @@ Qed.
 
 Theorem ZOdiv_mod_mult :
   forall n a b,
-  (ZOdiv (ZOmod n (a * b)) a) = ZOmod (ZOdiv n a) b.
+  (Z.quot (Z.rem n (a * b)) a) = Z.rem (Z.quot n a) b.
 Proof.
 intros n a b.
 destruct (Z_eq_dec a 0) as [Za|Za].
 rewrite Za.
-now rewrite 2!ZOdiv_0_r, ZOmod_0_l.
-assert (ZOmod n (a * b) = n + - (ZOdiv (ZOdiv n a) b * b) * a)%Z.
+now rewrite 2!Zquot_0_r, Zrem_0_l.
+assert (Z.rem n (a * b) = n + - (Z.quot (Z.quot n a) b * b) * a)%Z.
 rewrite (ZOmod_eq n (a * b)) at 1.
-rewrite ZOdiv_ZOdiv.
+rewrite Zquot_Zquot.
 ring.
 rewrite H.
-rewrite ZO_div_plus with (2 := Za).
+rewrite Z_quot_plus with (2 := Za).
 apply sym_eq.
 apply ZOmod_eq.
 rewrite <- H.
-apply ZOmod_sgn2.
+apply Zrem_sgn2.
 Qed.
 
 Theorem ZOdiv_small_abs :
   forall a b,
-  (Zabs a < b)%Z -> ZOdiv a b = Z0.
+  (Zabs a < b)%Z -> Z.quot a b = Z0.
 Proof.
 intros a b Ha.
 destruct (Zle_or_lt 0 a) as [H|H].
-apply ZOdiv_small.
+apply Zquot_small.
 split.
 exact H.
 now rewrite Zabs_eq in Ha.
 apply Zopp_inj.
-rewrite <- ZOdiv_opp_l, Zopp_0.
-apply ZOdiv_small.
+rewrite <- Zquot_opp_l, Zopp_0.
+apply Zquot_small.
 generalize (Zabs_non_eq a).
 omega.
 Qed.
 
 Theorem ZOmod_small_abs :
   forall a b,
-  (Zabs a < b)%Z -> ZOmod a b = a.
+  (Zabs a < b)%Z -> Z.rem a b = a.
 Proof.
 intros a b Ha.
 destruct (Zle_or_lt 0 a) as [H|H].
-apply ZOmod_small.
+apply Zrem_small.
 split.
 exact H.
 now rewrite Zabs_eq in Ha.
 apply Zopp_inj.
-rewrite <- ZOmod_opp_l.
-apply ZOmod_small.
+rewrite <- Zrem_opp_l.
+apply Zrem_small.
 generalize (Zabs_non_eq a).
 omega.
 Qed.
 
 Theorem ZOdiv_plus :
   forall a b c, (0 <= a * b)%Z ->
-  (ZOdiv (a + b) c = ZOdiv a c + ZOdiv b c + ZOdiv (ZOmod a c + ZOmod b c) c)%Z.
+  (Z.quot (a + b) c = Z.quot a c + Z.quot b c + Z.quot (Z.rem a c + Z.rem b c) c)%Z.
 Proof.
 intros a b c Hab.
 destruct (Z_eq_dec c 0) as [Zc|Zc].
-now rewrite Zc, 4!ZOdiv_0_r.
+now rewrite Zc, 4!Zquot_0_r.
 apply Zmult_reg_r with (1 := Zc).
 rewrite 2!Zmult_plus_distr_l.
-assert (forall d, ZOdiv d c * c = d - ZOmod d c)%Z.
+assert (forall d, Z.quot d c * c = d - Z.rem d c)%Z.
 intros d.
 rewrite ZOmod_eq.
 ring.
 rewrite 4!H.
-rewrite <- ZOplus_mod with (1 := Hab).
+rewrite <- Zplus_rem with (1 := Hab).
 ring.
 Qed.
 
@@ -543,14 +545,14 @@ Qed.
 
 Theorem Zsame_sign_odiv :
   forall u v, (0 <= v)%Z ->
-  (0 <= u * ZOdiv u v)%Z.
+  (0 <= u * Z.quot u v)%Z.
 Proof.
 intros u v Hv.
 apply Zsame_sign_imp ; intros Hu.
-apply ZO_div_pos with (2 := Hv).
+apply Z_quot_pos with (2 := Hv).
 now apply Zlt_le_weak.
-rewrite <- ZOdiv_opp_l.
-apply ZO_div_pos with (2 := Hv).
+rewrite <- Zquot_opp_l.
+apply Z_quot_pos with (2 := Hv).
 now apply Zlt_le_weak.
 Qed.
 
@@ -772,3 +774,156 @@ now apply Zabs_eq.
 Qed.
 
 End cond_Zopp.
+
+Section fast_pow_pos.
+
+Fixpoint Zfast_pow_pos (v : Z) (e : positive) : Z :=
+  match e with
+  | xH => v
+  | xO e' => Z.square (Zfast_pow_pos v e')
+  | xI e' => Zmult v (Z.square (Zfast_pow_pos v e'))
+  end.
+
+Theorem Zfast_pow_pos_correct :
+  forall v e, Zfast_pow_pos v e = Zpower_pos v e.
+Proof.
+intros v e.
+rewrite <- (Zmult_1_r (Zfast_pow_pos v e)).
+unfold Z.pow_pos.
+generalize 1%Z.
+revert v.
+induction e ; intros v f ; simpl.
+- rewrite <- 2!IHe.
+  rewrite Z.square_spec.
+  ring.
+- rewrite <- 2!IHe.
+  rewrite Z.square_spec.
+  apply eq_sym, Zmult_assoc.
+- apply eq_refl.
+Qed.
+
+End fast_pow_pos.
+
+Section faster_div.
+
+Lemma Zdiv_eucl_unique :
+  forall a b,
+  Zdiv_eucl a b = (Zdiv a b, Zmod a b).
+Proof.
+intros a b.
+unfold Zdiv, Zmod.
+now case Zdiv_eucl.
+Qed.
+
+Fixpoint Zpos_div_eucl_aux1 (a b : positive) {struct b} :=
+  match b with
+  | xO b' =>
+    match a with
+    | xO a' => let (q, r) := Zpos_div_eucl_aux1 a' b' in (q, 2 * r)%Z
+    | xI a' => let (q, r) := Zpos_div_eucl_aux1 a' b' in (q, 2 * r + 1)%Z
+    | xH => (Z0, Zpos a)
+    end
+  | xH => (Zpos a, Z0)
+  | xI _ => Z.pos_div_eucl a (Zpos b)
+  end.
+
+Lemma Zpos_div_eucl_aux1_correct :
+  forall a b,
+  Zpos_div_eucl_aux1 a b = Z.pos_div_eucl a (Zpos b).
+Proof.
+intros a b.
+revert a.
+induction b ; intros a.
+- easy.
+- change (Z.pos_div_eucl a (Zpos b~0)) with (Zdiv_eucl (Zpos a) (Zpos b~0)).
+  rewrite Zdiv_eucl_unique.
+  change (Zpos b~0) with (2 * Zpos b)%Z.
+  rewrite Z.rem_mul_r by easy.
+  rewrite <- Zdiv_Zdiv by easy.
+  destruct a as [a|a|].
+  + change (Zpos_div_eucl_aux1 a~1 b~0) with (let (q, r) := Zpos_div_eucl_aux1 a b in (q, 2 * r + 1)%Z).
+    rewrite IHb. clear IHb.
+    change (Z.pos_div_eucl a (Zpos b)) with (Zdiv_eucl (Zpos a) (Zpos b)).
+    rewrite Zdiv_eucl_unique.
+    change (Zpos a~1) with (1 + 2 * Zpos a)%Z.
+    rewrite (Zmult_comm 2 (Zpos a)).
+    rewrite Z_div_plus_full by easy.
+    apply f_equal.
+    rewrite Z_mod_plus_full.
+    apply Zplus_comm.
+  + change (Zpos_div_eucl_aux1 a~0 b~0) with (let (q, r) := Zpos_div_eucl_aux1 a b in (q, 2 * r)%Z).
+    rewrite IHb. clear IHb.
+    change (Z.pos_div_eucl a (Zpos b)) with (Zdiv_eucl (Zpos a) (Zpos b)).
+    rewrite Zdiv_eucl_unique.
+    change (Zpos a~0) with (2 * Zpos a)%Z.
+    rewrite (Zmult_comm 2 (Zpos a)).
+    rewrite Z_div_mult_full by easy.
+    apply f_equal.
+    now rewrite Z_mod_mult.
+  + easy.
+- change (Z.pos_div_eucl a 1) with (Zdiv_eucl (Zpos a) 1).
+  rewrite Zdiv_eucl_unique.
+  now rewrite Zdiv_1_r, Zmod_1_r.
+Qed.
+
+Definition Zpos_div_eucl_aux (a b : positive) :=
+  match Pos.compare a b with
+  | Lt => (Z0, Zpos a)
+  | Eq => (1%Z, Z0)
+  | Gt => Zpos_div_eucl_aux1 a b
+  end.
+
+Lemma Zpos_div_eucl_aux_correct :
+  forall a b,
+  Zpos_div_eucl_aux a b = Z.pos_div_eucl a (Zpos b).
+Proof.
+intros a b.
+unfold Zpos_div_eucl_aux.
+change (Z.pos_div_eucl a (Zpos b)) with (Zdiv_eucl (Zpos a) (Zpos b)).
+rewrite Zdiv_eucl_unique.
+case Pos.compare_spec ; intros H.
+now rewrite H, Z_div_same, Z_mod_same.
+now rewrite Zdiv_small, Zmod_small by (split ; easy).
+rewrite Zpos_div_eucl_aux1_correct.
+change (Z.pos_div_eucl a (Zpos b)) with (Zdiv_eucl (Zpos a) (Zpos b)).
+apply Zdiv_eucl_unique.
+Qed.
+
+Definition Zfast_div_eucl (a b : Z) :=
+  match a with
+  | Z0 => (0, 0)%Z
+  | Zpos a' =>
+    match b with
+    | Z0 => (0, 0)%Z
+    | Zpos b' => Zpos_div_eucl_aux a' b'
+    | Zneg b' =>
+      let (q, r) := Zpos_div_eucl_aux a' b' in
+      match r with
+      | Z0 => (-q, 0)%Z
+      | Zpos _ => (-(q + 1), (b + r))%Z
+      | Zneg _ => (-(q + 1), (b + r))%Z
+      end
+    end
+  | Zneg a' =>
+    match b with
+    | Z0 => (0, 0)%Z
+    | Zpos b' =>
+      let (q, r) := Zpos_div_eucl_aux a' b' in
+      match r with
+      | Z0 => (-q, 0)%Z
+      | Zpos _ => (-(q + 1), (b - r))%Z
+      | Zneg _ => (-(q + 1), (b - r))%Z
+      end
+    | Zneg b' => let (q, r) := Zpos_div_eucl_aux a' b' in (q, (-r)%Z)
+    end
+  end.
+
+Theorem Zfast_div_eucl_correct :
+  forall a b : Z,
+  Zfast_div_eucl a b = Zdiv_eucl a b.
+Proof.
+unfold Zfast_div_eucl.
+intros [|a|a] [|b|b] ; try rewrite Zpos_div_eucl_aux_correct ; easy.
+Qed.
+
+End faster_div.
diff --git a/flocq/Core/Fcore_digits.v b/flocq/Core/Fcore_digits.v
index 02c7a0e6..13174d29 100644
--- a/flocq/Core/Fcore_digits.v
+++ b/flocq/Core/Fcore_digits.v
@@ -18,8 +18,8 @@ COPYING file for more details.
 *)
 
 Require Import ZArith.
+Require Import Zquot.
 Require Import Fcore_Zaux.
-Require Import ZOdiv.
 
 (** Computes the number of bits (radix 2) of a positive integer.
 
@@ -40,7 +40,7 @@ Theorem digits2_Pnat_correct :
 Proof.
 intros n d. unfold d. clear.
 assert (Hp: forall m, (Zpower_nat 2 (S m) = 2 * Zpower_nat 2 m)%Z) by easy.
-induction n ; simpl.
+induction n ; simpl digits2_Pnat.
 rewrite Zpos_xI, 2!Hp.
 omega.
 rewrite (Zpos_xO n), 2!Hp.
@@ -52,7 +52,7 @@ Section Fcore_digits.
 
 Variable beta : radix.
 
-Definition Zdigit n k := ZOmod (ZOdiv n (Zpower beta k)) beta.
+Definition Zdigit n k := Z.rem (Z.quot n (Zpower beta k)) beta.
 
 Theorem Zdigit_lt :
   forall n k,
@@ -68,8 +68,8 @@ Theorem Zdigit_0 :
 Proof.
 intros k.
 unfold Zdigit.
-rewrite ZOdiv_0_l.
-apply ZOmod_0_l.
+rewrite Zquot_0_l.
+apply Zrem_0_l.
 Qed.
 
 Theorem Zdigit_opp :
@@ -78,8 +78,8 @@ Theorem Zdigit_opp :
 Proof.
 intros n k.
 unfold Zdigit.
-rewrite ZOdiv_opp_l.
-apply ZOmod_opp_l.
+rewrite Zquot_opp_l.
+apply Zrem_opp_l.
 Qed.
 
 Theorem Zdigit_ge_Zpower_pos :
@@ -89,8 +89,8 @@ Theorem Zdigit_ge_Zpower_pos :
 Proof.
 intros e n Hn k Hk.
 unfold Zdigit.
-rewrite ZOdiv_small.
-apply ZOmod_0_l.
+rewrite Zquot_small.
+apply Zrem_0_l.
 split.
 apply Hn.
 apply Zlt_le_trans with (1 := proj2 Hn).
@@ -134,12 +134,12 @@ Proof.
 intros e n He (Hn1,Hn2).
 unfold Zdigit.
 rewrite <- ZOdiv_mod_mult.
-rewrite ZOmod_small.
+rewrite Zrem_small.
 intros H.
 apply Zle_not_lt with (1 := Hn1).
-rewrite (ZO_div_mod_eq n (beta ^ e)).
+rewrite (Z.quot_rem' n (beta ^ e)).
 rewrite H, Zmult_0_r, Zplus_0_l.
-apply ZOmod_lt_pos_pos.
+apply Zrem_lt_pos_pos.
 apply Zle_trans with (2 := Hn1).
 apply Zpower_ge_0.
 now apply Zpower_gt_0.
@@ -178,10 +178,10 @@ pattern k' ; apply Zlt_0_ind with (2 := Hk').
 clear k' Hk'.
 intros k' IHk' Hk' k H.
 unfold Zdigit.
-apply (f_equal (fun x => ZOmod x beta)).
+apply (f_equal (fun x => Z.rem x beta)).
 pattern k at 1 ; replace k with (k - k' + k')%Z by ring.
 rewrite Zpower_plus with (2 := Hk').
-apply ZOdiv_mult_cancel_r.
+apply Zquot_mult_cancel_r.
 apply Zgt_not_eq.
 now apply Zpower_gt_0.
 now apply Zle_minus_le_0.
@@ -190,13 +190,13 @@ rewrite (Zdigit_lt n) by omega.
 unfold Zdigit.
 replace k' with (k' - k + k)%Z by ring.
 rewrite Zpower_plus with (2 := H0).
-rewrite Zmult_assoc, ZO_div_mult.
+rewrite Zmult_assoc, Z_quot_mult.
 replace (k' - k)%Z with (k' - k - 1 + 1)%Z by ring.
 rewrite Zpower_exp by omega.
 rewrite Zmult_assoc.
 change (Zpower beta 1) with (beta * 1)%Z.
 rewrite Zmult_1_r.
-apply ZO_mod_mult.
+apply Z_rem_mult.
 apply Zgt_not_eq.
 now apply Zpower_gt_0.
 apply Zle_minus_le_0.
@@ -209,24 +209,24 @@ Qed.
 
 Theorem Zdigit_div_pow :
   forall n k k', (0 <= k)%Z -> (0 <= k')%Z ->
-  Zdigit (ZOdiv n (Zpower beta k')) k = Zdigit n (k + k').
+  Zdigit (Z.quot n (Zpower beta k')) k = Zdigit n (k + k').
 Proof.
 intros n k k' Hk Hk'.
 unfold Zdigit.
-rewrite ZOdiv_ZOdiv.
+rewrite Zquot_Zquot.
 rewrite Zplus_comm.
 now rewrite Zpower_plus.
 Qed.
 
 Theorem Zdigit_mod_pow :
   forall n k k', (k < k')%Z ->
-  Zdigit (ZOmod n (Zpower beta k')) k = Zdigit n k.
+  Zdigit (Z.rem n (Zpower beta k')) k = Zdigit n k.
 Proof.
 intros n k k' Hk.
 destruct (Zle_or_lt 0 k) as [H|H].
 unfold Zdigit.
 rewrite <- 2!ZOdiv_mod_mult.
-apply (f_equal (fun x => ZOdiv x (beta ^ k))).
+apply (f_equal (fun x => Z.quot x (beta ^ k))).
 replace k' with (k + 1 + (k' - (k + 1)))%Z by ring.
 rewrite Zpower_exp by omega.
 rewrite Zmult_comm.
@@ -239,15 +239,15 @@ Qed.
 
 Theorem Zdigit_mod_pow_out :
   forall n k k', (0 <= k' <= k)%Z ->
-  Zdigit (ZOmod n (Zpower beta k')) k = Z0.
+  Zdigit (Z.rem n (Zpower beta k')) k = Z0.
 Proof.
 intros n k k' Hk.
 unfold Zdigit.
 rewrite ZOdiv_small_abs.
-apply ZOmod_0_l.
+apply Zrem_0_l.
 apply Zlt_le_trans with (Zpower beta k').
 rewrite <- (Zabs_eq (beta ^ k')) at 2 by apply Zpower_ge_0.
-apply ZOmod_lt.
+apply Zrem_lt.
 apply Zgt_not_eq.
 now apply Zpower_gt_0.
 now apply Zpower_le.
@@ -261,12 +261,12 @@ Fixpoint Zsum_digit f k :=
 
 Theorem Zsum_digit_digit :
   forall n k,
-  Zsum_digit (Zdigit n) k = ZOmod n (Zpower beta (Z_of_nat k)).
+  Zsum_digit (Zdigit n) k = Z.rem n (Zpower beta (Z_of_nat k)).
 Proof.
 intros n.
 induction k.
 apply sym_eq.
-apply ZOmod_1_r.
+apply Zrem_1_r.
 simpl Zsum_digit.
 rewrite IHk.
 unfold Zdigit.
@@ -276,7 +276,7 @@ rewrite Zmult_comm.
 replace (beta ^ Z_of_nat k * beta)%Z with (Zpower beta (Z_of_nat (S k))).
 rewrite Zplus_comm, Zmult_comm.
 apply sym_eq.
-apply ZO_div_mod_eq.
+apply Z.quot_rem'.
 rewrite inj_S.
 rewrite <- (Zmult_1_r beta) at 3.
 apply Zpower_plus.
@@ -348,17 +348,17 @@ Qed.
 Theorem ZOmod_plus_pow_digit :
   forall u v n, (0 <= u * v)%Z ->
   (forall k, (0 <= k < n)%Z -> Zdigit u k = Z0 \/ Zdigit v k = Z0) ->
-  ZOmod (u + v) (Zpower beta n) = (ZOmod u (Zpower beta n) + ZOmod v (Zpower beta n))%Z.
+  Z.rem (u + v) (Zpower beta n) = (Z.rem u (Zpower beta n) + Z.rem v (Zpower beta n))%Z.
 Proof.
 intros u v n Huv Hd.
 destruct (Zle_or_lt 0 n) as [Hn|Hn].
-rewrite ZOplus_mod with (1 := Huv).
+rewrite Zplus_rem with (1 := Huv).
 apply ZOmod_small_abs.
 generalize (Zle_refl n).
 pattern n at -2 ; rewrite <- Zabs_eq with (1 := Hn).
 rewrite <- (inj_Zabs_nat n).
 induction (Zabs_nat n) as [|p IHp].
-now rewrite 2!ZOmod_1_r.
+now rewrite 2!Zrem_1_r.
 rewrite <- 2!Zsum_digit_digit.
 simpl Zsum_digit.
 rewrite inj_S.
@@ -385,7 +385,7 @@ apply refl_equal.
 apply Zle_bool_imp_le.
 apply beta.
 replace (Zsucc (beta - 1)) with (Zabs beta).
-apply ZOmod_lt.
+apply Zrem_lt.
 now apply Zgt_not_eq.
 rewrite Zabs_eq.
 apply Zsucc_pred.
@@ -407,29 +407,29 @@ now rewrite Zmult_1_r.
 apply Zle_0_nat.
 easy.
 destruct n as [|n|n] ; try easy.
-now rewrite 3!ZOmod_0_r.
+now rewrite 3!Zrem_0_r.
 Qed.
 
 Theorem ZOdiv_plus_pow_digit :
   forall u v n, (0 <= u * v)%Z ->
   (forall k, (0 <= k < n)%Z -> Zdigit u k = Z0 \/ Zdigit v k = Z0) ->
-  ZOdiv (u + v) (Zpower beta n) = (ZOdiv u (Zpower beta n) + ZOdiv v (Zpower beta n))%Z.
+  Z.quot (u + v) (Zpower beta n) = (Z.quot u (Zpower beta n) + Z.quot v (Zpower beta n))%Z.
 Proof.
 intros u v n Huv Hd.
-rewrite <- (Zplus_0_r (ZOdiv u (Zpower beta n) + ZOdiv v (Zpower beta n))).
+rewrite <- (Zplus_0_r (Z.quot u (Zpower beta n) + Z.quot v (Zpower beta n))).
 rewrite ZOdiv_plus with (1 := Huv).
 rewrite <- ZOmod_plus_pow_digit by assumption.
 apply f_equal.
 destruct (Zle_or_lt 0 n) as [Hn|Hn].
 apply ZOdiv_small_abs.
 rewrite <- Zabs_eq.
-apply ZOmod_lt.
+apply Zrem_lt.
 apply Zgt_not_eq.
 now apply Zpower_gt_0.
 apply Zpower_ge_0.
 clear -Hn.
 destruct n as [|n|n] ; try easy.
-apply ZOdiv_0_r.
+apply Zquot_0_r.
 Qed.
 
 Theorem Zdigit_plus :
@@ -447,11 +447,11 @@ change (beta * 1)%Z with (beta ^1)%Z.
 apply ZOmod_plus_pow_digit.
 apply Zsame_sign_trans_weak with v.
 intros Zv ; rewrite Zv.
-apply ZOdiv_0_l.
+apply Zquot_0_l.
 rewrite Zmult_comm.
 apply Zsame_sign_trans_weak with u.
 intros Zu ; rewrite Zu.
-apply ZOdiv_0_l.
+apply Zquot_0_l.
 now rewrite Zmult_comm.
 apply Zsame_sign_odiv.
 apply Zpower_ge_0.
@@ -467,7 +467,7 @@ now rewrite 3!Zdigit_lt.
 Qed.
 
 Definition Zscale n k :=
-  if Zle_bool 0 k then (n * Zpower beta k)%Z else ZOdiv n (Zpower beta (-k)).
+  if Zle_bool 0 k then (n * Zpower beta k)%Z else Z.quot n (Zpower beta (-k)).
 
 Theorem Zdigit_scale :
   forall n k k', (0 <= k')%Z ->
@@ -489,7 +489,7 @@ intros k.
 unfold Zscale.
 case Zle_bool.
 apply Zmult_0_l.
-apply ZOdiv_0_l.
+apply Zquot_0_l.
 Qed.
 
 Theorem Zsame_sign_scale :
@@ -523,13 +523,13 @@ case Zle_bool_spec ; intros Hk''.
 pattern k at 1 ; replace k with (k + k' + -k')%Z by ring.
 assert (0 <= -k')%Z by omega.
 rewrite Zpower_plus by easy.
-rewrite Zmult_assoc, ZO_div_mult.
+rewrite Zmult_assoc, Z_quot_mult.
 apply refl_equal.
 apply Zgt_not_eq.
 now apply Zpower_gt_0.
 replace (-k')%Z with (-(k+k') + k)%Z by ring.
 rewrite Zpower_plus with (2 := Hk).
-apply ZOdiv_mult_cancel_r.
+apply Zquot_mult_cancel_r.
 apply Zgt_not_eq.
 now apply Zpower_gt_0.
 omega.
@@ -546,7 +546,7 @@ now apply Zscale_mul_pow.
 Qed.
 
 Definition Zslice n k1 k2 :=
-  if Zle_bool 0 k2 then ZOmod (Zscale n (-k1)) (Zpower beta k2) else Z0.
+  if Zle_bool 0 k2 then Z.rem (Zscale n (-k1)) (Zpower beta k2) else Z0.
 
 Theorem Zdigit_slice :
   forall n k1 k2 k, (0 <= k < k2)%Z ->
@@ -582,7 +582,7 @@ intros k k'.
 unfold Zslice.
 case Zle_bool.
 rewrite Zscale_0.
-apply ZOmod_0_l.
+apply Zrem_0_l.
 apply refl_equal.
 Qed.
 
@@ -595,10 +595,10 @@ unfold Zslice.
 case Zle_bool.
 apply Zsame_sign_trans_weak with (Zscale n (-k)).
 intros H ; rewrite H.
-apply ZOmod_0_l.
+apply Zrem_0_l.
 apply Zsame_sign_scale.
 rewrite Zmult_comm.
-apply ZOmod_sgn2.
+apply Zrem_sgn2.
 now rewrite Zmult_0_r.
 Qed.
 
@@ -642,26 +642,26 @@ Qed.
 
 Theorem Zslice_div_pow :
   forall n k k1 k2, (0 <= k)%Z -> (0 <= k1)%Z ->
-  Zslice (ZOdiv n (Zpower beta k)) k1 k2 = Zslice n (k1 + k) k2.
+  Zslice (Z.quot n (Zpower beta k)) k1 k2 = Zslice n (k1 + k) k2.
 Proof.
 intros n k k1 k2 Hk Hk1.
 unfold Zslice.
 case Zle_bool_spec ; intros Hk2.
 2: apply refl_equal.
-apply (f_equal (fun x => ZOmod x (beta ^ k2))).
+apply (f_equal (fun x => Z.rem x (beta ^ k2))).
 unfold Zscale.
 case Zle_bool_spec ; intros Hk1'.
 replace k1 with Z0 by omega.
 case Zle_bool_spec ; intros Hk'.
 replace k with Z0 by omega.
 simpl.
-now rewrite ZOdiv_1_r.
+now rewrite Zquot_1_r.
 rewrite Zopp_involutive.
 apply Zmult_1_r.
 rewrite Zle_bool_false by omega.
 rewrite 2!Zopp_involutive, Zplus_comm.
 rewrite Zpower_plus by assumption.
-apply ZOdiv_ZOdiv.
+apply Zquot_Zquot.
 Qed.
 
 Theorem Zslice_scale :
@@ -678,7 +678,7 @@ Qed.
 
 Theorem Zslice_div_pow_scale :
   forall n k k1 k2, (0 <= k)%Z ->
-  Zslice (ZOdiv n (Zpower beta k)) k1 k2 = Zscale (Zslice n k (k1 + k2)) (-k1).
+  Zslice (Z.quot n (Zpower beta k)) k1 k2 = Zscale (Zslice n k (k1 + k2)) (-k1).
 Proof.
 intros n k k1 k2 Hk.
 apply Zdigit_ext.
@@ -746,7 +746,6 @@ Qed.
 Section digits_aux.
 
 Variable p : Z.
-Hypothesis Hp : (0 <= p)%Z.
 
 Fixpoint Zdigits_aux (nb pow : Z) (n : nat) { struct n } : Z :=
   match n with
@@ -755,6 +754,7 @@ Fixpoint Zdigits_aux (nb pow : Z) (n : nat) { struct n } : Z :=
   end.
 
 End digits_aux.
+
 (** Number of digits of an integer *)
 Definition Zdigits n :=
   match n with
@@ -822,6 +822,20 @@ easy.
 apply Zle_succ_le with (1 := Hv).
 Qed.
 
+Theorem Zdigits_unique :
+  forall n d,
+  (Zpower beta (d - 1) <= Zabs n < Zpower beta d)%Z ->
+  Zdigits n = d.
+Proof.
+intros n d Hd.
+assert (Hd' := Zdigits_correct n).
+apply Zle_antisym.
+apply (Zpower_lt_Zpower beta).
+now apply Zle_lt_trans with (Zabs n).
+apply (Zpower_lt_Zpower beta).
+now apply Zle_lt_trans with (Zabs n).
+Qed.
+
 Theorem Zdigits_abs :
   forall n, Zdigits (Zabs n) = Zdigits n.
 Proof.
@@ -887,13 +901,278 @@ Proof.
 intros n k l Hl.
 unfold Zslice.
 rewrite Zle_bool_true with (1 := Hl).
-destruct (Zdigits_correct (ZOmod (Zscale n (- k)) (Zpower beta l))) as (H1,H2).
+destruct (Zdigits_correct (Z.rem (Zscale n (- k)) (Zpower beta l))) as (H1,H2).
 apply Zpower_lt_Zpower with beta.
 apply Zle_lt_trans with (1 := H1).
 rewrite <- (Zabs_eq (beta ^ l)) at 2 by apply Zpower_ge_0.
-apply ZOmod_lt.
+apply Zrem_lt.
 apply Zgt_not_eq.
 now apply Zpower_gt_0.
 Qed.
 
+Theorem Zdigits_mult_Zpower :
+  forall m e,
+  m <> Z0 -> (0 <= e)%Z ->
+  Zdigits (m * Zpower beta e) = (Zdigits m + e)%Z.
+Proof.
+intros m e Hm He.
+assert (H := Zdigits_correct m).
+apply Zdigits_unique.
+rewrite Z.abs_mul, Z.abs_pow, (Zabs_eq beta).
+2: now apply Zlt_le_weak, radix_gt_0.
+split.
+replace (Zdigits m + e - 1)%Z with (Zdigits m - 1 + e)%Z by ring.
+rewrite Zpower_plus with (2 := He).
+apply Zmult_le_compat_r.
+apply H.
+apply Zpower_ge_0.
+now apply Zlt_0_le_0_pred, Zdigits_gt_0.
+rewrite Zpower_plus with (2 := He).
+apply Zmult_lt_compat_r.
+now apply Zpower_gt_0.
+apply H.
+now apply Zlt_le_weak, Zdigits_gt_0.
+Qed.
+
+Theorem Zdigits_Zpower :
+  forall e,
+  (0 <= e)%Z ->
+  Zdigits (Zpower beta e) = (e + 1)%Z.
+Proof.
+intros e He.
+rewrite <- (Zmult_1_l (Zpower beta e)).
+rewrite Zdigits_mult_Zpower ; try easy.
+apply Zplus_comm.
+Qed.
+
+Theorem Zdigits_le :
+  forall x y,
+  (0 <= x)%Z -> (x <= y)%Z ->
+  (Zdigits x <= Zdigits y)%Z.
+Proof.
+intros x y Zx Hxy.
+assert (Hx := Zdigits_correct x).
+assert (Hy := Zdigits_correct y).
+apply (Zpower_lt_Zpower beta).
+zify ; omega.
+Qed.
+
+Theorem lt_Zdigits :
+  forall x y,
+  (0 <= y)%Z ->
+  (Zdigits x < Zdigits y)%Z ->
+  (x < y)%Z.
+Proof.
+intros x y Hy.
+cut (y <= x -> Zdigits y <= Zdigits x)%Z. omega.
+now apply Zdigits_le.
+Qed.
+
+Theorem Zpower_le_Zdigits :
+  forall e x,
+  (e < Zdigits x)%Z ->
+  (Zpower beta e <= Zabs x)%Z.
+Proof.
+intros e x Hex.
+destruct (Zdigits_correct x) as [H1 H2].
+apply Zle_trans with (2 := H1).
+apply Zpower_le.
+clear -Hex ; omega.
+Qed.
+
+Theorem Zdigits_le_Zpower :
+  forall e x,
+  (Zabs x < Zpower beta e)%Z ->
+  (Zdigits x <= e)%Z.
+Proof.
+intros e x.
+generalize (Zpower_le_Zdigits e x).
+omega.
+Qed.
+
+Theorem Zpower_gt_Zdigits :
+  forall e x,
+  (Zdigits x <= e)%Z ->
+  (Zabs x < Zpower beta e)%Z.
+Proof.
+intros e x Hex.
+destruct (Zdigits_correct x) as [H1 H2].
+apply Zlt_le_trans with (1 := H2).
+now apply Zpower_le.
+Qed.
+
+Theorem Zdigits_gt_Zpower :
+  forall e x,
+  (Zpower beta e <= Zabs x)%Z ->
+  (e < Zdigits x)%Z.
+Proof.
+intros e x Hex.
+generalize (Zpower_gt_Zdigits e x).
+omega.
+Qed.
+
+(** Characterizes the number digits of a product.
+
+This strong version is needed for proofs of division and square root
+algorithms, since they involve operation remainders.
+*)
+
+Theorem Zdigits_mult_strong :
+  forall x y,
+  (0 <= x)%Z -> (0 <= y)%Z ->
+  (Zdigits (x + y + x * y) <= Zdigits x + Zdigits y)%Z.
+Proof.
+intros x y Hx Hy.
+apply Zdigits_le_Zpower.
+rewrite Zabs_eq.
+apply Zlt_le_trans with ((x + 1) * (y + 1))%Z.
+ring_simplify.
+apply Zle_lt_succ, Zle_refl.
+rewrite Zpower_plus by apply Zdigits_ge_0.
+apply Zmult_le_compat.
+apply Zlt_le_succ.
+rewrite <- (Zabs_eq x) at 1 by easy.
+apply Zdigits_correct.
+apply Zlt_le_succ.
+rewrite <- (Zabs_eq y) at 1 by easy.
+apply Zdigits_correct.
+clear -Hx ; omega.
+clear -Hy ; omega.
+change Z0 with (0 + 0 + 0)%Z.
+apply Zplus_le_compat.
+now apply Zplus_le_compat.
+now apply Zmult_le_0_compat.
+Qed.
+
+Theorem Zdigits_mult :
+  forall x y,
+  (Zdigits (x * y) <= Zdigits x + Zdigits y)%Z.
+Proof.
+intros x y.
+rewrite <- Zdigits_abs.
+rewrite <- (Zdigits_abs x).
+rewrite <- (Zdigits_abs y).
+apply Zle_trans with (Zdigits (Zabs x + Zabs y + Zabs x * Zabs y)).
+apply Zdigits_le.
+apply Zabs_pos.
+rewrite Zabs_Zmult.
+generalize (Zabs_pos x) (Zabs_pos y).
+omega.
+apply Zdigits_mult_strong ; apply Zabs_pos.
+Qed.
+
+Theorem Zdigits_mult_ge :
+  forall x y,
+  (x <> 0)%Z -> (y <> 0)%Z ->
+  (Zdigits x + Zdigits y - 1 <= Zdigits (x * y))%Z.
+Proof.
+intros x y Zx Zy.
+cut ((Zdigits x - 1) + (Zdigits y - 1) < Zdigits (x * y))%Z. omega.
+apply Zdigits_gt_Zpower.
+rewrite Zabs_Zmult.
+rewrite Zpower_exp.
+apply Zmult_le_compat.
+apply Zpower_le_Zdigits.
+apply Zlt_pred.
+apply Zpower_le_Zdigits.
+apply Zlt_pred.
+apply Zpower_ge_0.
+apply Zpower_ge_0.
+generalize (Zdigits_gt_0 x). omega.
+generalize (Zdigits_gt_0 y). omega.
+Qed.
+
+Theorem Zdigits_div_Zpower :
+  forall m e,
+  (0 <= m)%Z ->
+  (0 <= e <= Zdigits m)%Z ->
+  Zdigits (m / Zpower beta e) = (Zdigits m - e)%Z.
+Proof.
+intros m e Hm He.
+assert (H := Zdigits_correct m).
+apply Zdigits_unique.
+destruct (Zle_lt_or_eq _ _ (proj2 He)) as [He'|He'].
+  rewrite Zabs_eq in H by easy.
+  destruct H as [H1 H2].
+  rewrite Zabs_eq.
+  split.
+  replace (Zdigits m - e - 1)%Z with (Zdigits m - 1 - e)%Z by ring.
+  rewrite Z.pow_sub_r.
+  2: apply Zgt_not_eq, radix_gt_0.
+  2: clear -He He' ; omega.
+  apply Z_div_le with (2 := H1).
+  now apply Zlt_gt, Zpower_gt_0.
+  apply Zmult_lt_reg_r with (Zpower beta e).
+  now apply Zpower_gt_0.
+  apply Zle_lt_trans with m.
+  rewrite Zmult_comm.
+  apply Z_mult_div_ge.
+  now apply Zlt_gt, Zpower_gt_0.
+  rewrite <- Zpower_plus.
+  now replace (Zdigits m - e + e)%Z with (Zdigits m) by ring.
+  now apply Zle_minus_le_0.
+  apply He.
+  apply Z_div_pos with (2 := Hm).
+  now apply Zlt_gt, Zpower_gt_0.
+rewrite He'.
+rewrite (Zeq_minus _ (Zdigits m)) by reflexivity.
+simpl.
+rewrite Zdiv_small.
+easy.
+split.
+exact Hm.
+now rewrite <- (Zabs_eq m) at 1.
+Qed.
+
 End Fcore_digits.
+
+Section Zdigits2.
+
+Theorem Z_of_nat_S_digits2_Pnat :
+  forall m : positive,
+  Z_of_nat (S (digits2_Pnat m)) = Zdigits radix2 (Zpos m).
+Proof.
+intros m.
+apply eq_sym, Zdigits_unique.
+rewrite <- Zpower_nat_Z.
+rewrite Nat2Z.inj_succ.
+change (_ - 1)%Z with (Zpred (Zsucc (Z.of_nat (digits2_Pnat m)))).
+rewrite <- Zpred_succ.
+rewrite <- Zpower_nat_Z.
+apply digits2_Pnat_correct.
+Qed.
+
+Fixpoint digits2_pos (n : positive) : positive :=
+  match n with
+  | xH => xH
+  | xO p => Psucc (digits2_pos p)
+  | xI p => Psucc (digits2_pos p)
+  end.
+
+Theorem Zpos_digits2_pos :
+  forall m : positive,
+  Zpos (digits2_pos m) = Zdigits radix2 (Zpos m).
+Proof.
+intros m.
+rewrite <- Z_of_nat_S_digits2_Pnat.
+unfold Z.of_nat.
+apply f_equal.
+induction m ; simpl ; try easy ;
+  apply f_equal, IHm.
+Qed.
+
+Definition Zdigits2 n :=
+  match n with
+  | Z0 => n
+  | Zpos p => Zpos (digits2_pos p)
+  | Zneg p => Zpos (digits2_pos p)
+  end.
+
+Lemma Zdigits2_Zdigits :
+  forall n, Zdigits2 n = Zdigits radix2 n.
+Proof.
+intros [|p|p] ; try easy ;
+  apply Zpos_digits2_pos.
+Qed.
+
+End Zdigits2.
diff --git a/flocq/Core/Fcore_generic_fmt.v b/flocq/Core/Fcore_generic_fmt.v
index b04cf3d0..45729f2a 100644
--- a/flocq/Core/Fcore_generic_fmt.v
+++ b/flocq/Core/Fcore_generic_fmt.v
@@ -1380,8 +1380,6 @@ contradict Fx.
 apply generic_format_round...
 Qed.
 
-
-
 Theorem round_UP_small_pos :
   forall x ex,
   (bpow (ex - 1) <= x < bpow ex)%R ->
@@ -1793,7 +1791,7 @@ rewrite Z2R_plus. simpl.
 destruct (Rcompare_spec (x - Z2R (Zfloor x)) (/ 2)) as [H1|H1|H1] ; apply sym_eq.
 (* . *)
 apply Rcompare_Lt.
-apply Rplus_lt_reg_r with (x - Z2R (Zfloor x))%R.
+apply Rplus_lt_reg_l with (x - Z2R (Zfloor x))%R.
 replace (x - Z2R (Zfloor x) + (x - Z2R (Zfloor x)))%R with ((x - Z2R (Zfloor x)) * 2)%R by ring.
 replace (x - Z2R (Zfloor x) + (Z2R (Zfloor x) + 1 - x))%R with (/2 * 2)%R by field.
 apply Rmult_lt_compat_r with (2 := H1).
@@ -1805,7 +1803,7 @@ rewrite H1.
 field.
 (* . *)
 apply Rcompare_Gt.
-apply Rplus_lt_reg_r with (x - Z2R (Zfloor x))%R.
+apply Rplus_lt_reg_l with (x - Z2R (Zfloor x))%R.
 replace (x - Z2R (Zfloor x) + (x - Z2R (Zfloor x)))%R with ((x - Z2R (Zfloor x)) * 2)%R by ring.
 replace (x - Z2R (Zfloor x) + (Z2R (Zfloor x) + 1 - x))%R with (/2 * 2)%R by field.
 apply Rmult_lt_compat_r with (2 := H1).
@@ -1823,7 +1821,7 @@ rewrite Z2R_plus. simpl.
 destruct (Rcompare_spec (Z2R (Zfloor x) + 1 - x) (/ 2)) as [H1|H1|H1] ; apply sym_eq.
 (* . *)
 apply Rcompare_Lt.
-apply Rplus_lt_reg_r with (Z2R (Zfloor x) + 1 - x)%R.
+apply Rplus_lt_reg_l with (Z2R (Zfloor x) + 1 - x)%R.
 replace (Z2R (Zfloor x) + 1 - x + (Z2R (Zfloor x) + 1 - x))%R with ((Z2R (Zfloor x) + 1 - x) * 2)%R by ring.
 replace (Z2R (Zfloor x) + 1 - x + (x - Z2R (Zfloor x)))%R with (/2 * 2)%R by field.
 apply Rmult_lt_compat_r with (2 := H1).
@@ -1835,7 +1833,7 @@ rewrite H1.
 field.
 (* . *)
 apply Rcompare_Gt.
-apply Rplus_lt_reg_r with (Z2R (Zfloor x) + 1 - x)%R.
+apply Rplus_lt_reg_l with (Z2R (Zfloor x) + 1 - x)%R.
 replace (Z2R (Zfloor x) + 1 - x + (Z2R (Zfloor x) + 1 - x))%R with ((Z2R (Zfloor x) + 1 - x) * 2)%R by ring.
 replace (Z2R (Zfloor x) + 1 - x + (x - Z2R (Zfloor x)))%R with (/2 * 2)%R by field.
 apply Rmult_lt_compat_r with (2 := H1).
@@ -1861,11 +1859,11 @@ rewrite Zceil_floor_neq.
 rewrite Z2R_plus.
 simpl.
 apply Ropp_lt_cancel.
-apply Rplus_lt_reg_r with R1.
+apply Rplus_lt_reg_l with R1.
 replace (1 + -/2)%R with (/2)%R by field.
 now replace (1 + - (Z2R (Zfloor x) + 1 - x))%R with (x - Z2R (Zfloor x))%R by ring.
 apply Rlt_not_eq.
-apply Rplus_lt_reg_r with (- Z2R (Zfloor x))%R.
+apply Rplus_lt_reg_l with (- Z2R (Zfloor x))%R.
 apply Rlt_trans with (/2)%R.
 rewrite Rplus_opp_l.
 apply Rinv_0_lt_compat.
@@ -1897,7 +1895,7 @@ rewrite Hx.
 rewrite Rabs_minus_sym.
 now replace (1 - /2)%R with (/2)%R by field.
 apply Rlt_not_eq.
-apply Rplus_lt_reg_r with (- Z2R (Zfloor x))%R.
+apply Rplus_lt_reg_l with (- Z2R (Zfloor x))%R.
 rewrite Rplus_opp_l, Rplus_comm.
 fold (x - Z2R (Zfloor x))%R.
 rewrite Hx.
@@ -2019,6 +2017,49 @@ apply Rgt_not_eq.
 apply bpow_gt_0.
 Qed.
 
+Lemma round_N_really_small_pos :
+  forall x,
+  forall ex,
+  (Fcore_Raux.bpow beta (ex - 1) <= x < Fcore_Raux.bpow beta ex)%R ->
+  (ex < fexp ex)%Z ->
+  (round Znearest x = 0)%R.
+Proof.
+intros x ex Hex Hf.
+unfold round, F2R, scaled_mantissa, canonic_exp; simpl.
+apply (Rmult_eq_reg_r (bpow (- fexp (ln_beta beta x))));
+  [|now apply Rgt_not_eq; apply bpow_gt_0].
+rewrite Rmult_0_l, Rmult_assoc, <- bpow_plus.
+replace (_ + - _)%Z with 0%Z by ring; simpl; rewrite Rmult_1_r.
+change 0%R with (Z2R 0); apply f_equal.
+apply Znearest_imp.
+simpl; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r.
+assert (H : (x >= 0)%R).
+{ apply Rle_ge; apply Rle_trans with (bpow (ex - 1)); [|exact (proj1 Hex)].
+  now apply bpow_ge_0. }
+assert (H' : (x * bpow (- fexp (ln_beta beta x)) >= 0)%R).
+{ apply Rle_ge; apply Rmult_le_pos.
+  - now apply Rge_le.
+  - now apply bpow_ge_0. }
+rewrite Rabs_right; [|exact H'].
+apply (Rmult_lt_reg_r (bpow (fexp (ln_beta beta x)))); [now apply bpow_gt_0|].
+rewrite Rmult_assoc, <- bpow_plus.
+replace (- _ + _)%Z with 0%Z by ring; simpl; rewrite Rmult_1_r.
+apply (Rlt_le_trans _ _ _ (proj2 Hex)).
+apply Rle_trans with (bpow (fexp (ln_beta beta x) - 1)).
+- apply bpow_le.
+  rewrite (ln_beta_unique beta x ex); [omega|].
+  now rewrite Rabs_right.
+- unfold Zminus; rewrite bpow_plus.
+  rewrite Rmult_comm.
+  apply Rmult_le_compat_r; [now apply bpow_ge_0|].
+  unfold Fcore_Raux.bpow, Z.pow_pos; simpl.
+  rewrite Zmult_1_r.
+  apply Rinv_le; [exact Rlt_0_2|].
+  change 2%R with (Z2R 2); apply Z2R_le.
+  destruct beta as (beta_val,beta_prop).
+  now apply Zle_bool_imp_le.
+Qed.
+
 End Znearest.
 
 Section rndNA.
@@ -2324,6 +2365,37 @@ End Generic.
 
 Notation ZnearestA := (Znearest (Zle_bool 0)).
 
+Section rndNA_opp.
+
+Lemma round_NA_opp :
+  forall beta : radix,
+  forall (fexp : Z -> Z),
+  forall x,
+  (round beta fexp ZnearestA (- x) = - round beta fexp ZnearestA x)%R.
+Proof.
+intros beta fexp x.
+rewrite round_N_opp.
+apply Ropp_eq_compat.
+apply round_ext.
+clear x; intro x.
+unfold Znearest.
+case_eq (Rcompare (x - Z2R (Zfloor x)) (/ 2)); intro C;
+[|reflexivity|reflexivity].
+apply Rcompare_Eq_inv in C.
+assert (H : negb (0 <=? - (Zfloor x + 1))%Z = (0 <=? Zfloor x)%Z);
+  [|now rewrite H].
+rewrite negb_Zle_bool.
+case_eq (0 <=? Zfloor x)%Z; intro C'.
+- apply Zle_bool_imp_le in C'.
+  apply Zlt_bool_true.
+  omega.
+- rewrite Z.leb_gt in C'.
+  apply Zlt_bool_false.
+  omega.
+Qed.
+
+End rndNA_opp.
+
 (** Notations for backward-compatibility with Flocq 1.4. *)
 Notation rndDN := Zfloor (only parsing).
 Notation rndUP := Zceil (only parsing).
diff --git a/flocq/Core/Fcore_ulp.v b/flocq/Core/Fcore_ulp.v
index 07ef3ec7..04bed01c 100644
--- a/flocq/Core/Fcore_ulp.v
+++ b/flocq/Core/Fcore_ulp.v
@@ -325,7 +325,7 @@ 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_r with (round beta fexp Zfloor x).
+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).