Upgrade to Flocq 4.0.

1 files changed, 35 insertions, 8 deletions

diff --git a/flocq/Core/Raux.v b/flocq/Core/Raux.v
index 221d84d6..a418bf19 100644
--- a/flocq/Core/Raux.v
+++ b/flocq/Core/Raux.v
@@ -18,9 +18,10 @@ COPYING file for more details.
 *)
 
 (** * Missing definitions/lemmas *)
-Require Import Psatz.
-Require Export Reals ZArith.
-Require Export Zaux.
+
+From Coq Require Import Psatz Reals ZArith.
+
+Require Import Zaux.
 
 Section Rmissing.
 
@@ -1317,9 +1318,9 @@ rewrite Ropp_inv_permute with (1 := Zy').
 rewrite <- 2!opp_IZR.
 rewrite <- Zmod_opp_opp.
 apply H.
-clear -Hy. lia.
+clear -Hy ; lia.
 apply H.
-clear -Zy Hy. lia.
+clear -Zy Hy ; lia.
 (* *)
 split.
 pattern (IZR (x / y)) at 1 ; rewrite <- Rplus_0_r.
@@ -1912,7 +1913,7 @@ apply bpow_le.
 now apply Zlt_le_weak.
 apply IZR_le.
 clear -Zm.
-zify ; lia.
+lia.
 Qed.
 
 Lemma mag_mult :
@@ -2040,6 +2041,33 @@ replace (ex - 1 - 1)%Z with (ex - 2)%Z by ring.
 now apply Rabs_ge; right.
 Qed.
 
+Theorem mag_plus_ge :
+  forall x y,
+  (x <> 0)%R ->
+  (mag y <= mag x - 2)%Z ->
+  (mag x - 1 <= mag (x + y))%Z.
+Proof.
+intros x y Zx.
+destruct (Req_dec y 0) as [Zy|Zy].
+{ intros _.
+  rewrite Zy, Rplus_0_r.
+  lia. }
+rewrite <- (mag_abs x), <- (mag_abs y).
+intros Hm.
+assert (H: Rabs x <> Rabs y).
+{ intros H.
+  apply Zlt_not_le with (2 := Hm).
+  rewrite H.
+  lia. }
+apply mag_minus_lb in Hm ; try now apply Rabs_pos_lt.
+apply Z.le_trans with (1 := Hm).
+apply mag_le_abs.
+now apply Rminus_eq_contra.
+rewrite <- (Ropp_involutive y).
+rewrite Rabs_Ropp.
+apply Rabs_triang_inv2.
+Qed.
+
 Lemma mag_div :
   forall x y : R,
   x <> 0%R -> y <> 0%R ->
@@ -2335,8 +2363,7 @@ refine (Rle_not_lt _ _ (lub (/ (INR (S N) + 1))%R _) _).
   intros Hy.
   refine (H _ _ Py).
   apply INR_lt in Hy.
-  clear -Hy HyN.
-  lia.
+  clear -Hy HyN ; lia.
   now apply Rlt_le, Rinv_0_lt_compat.
 rewrite S_INR, HN.
 ring_simplify (IZR (up (/ l)) - 1 + 1)%R.