From b08a818cbc7872b1a062a80ea478b2e32e3a3746 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Wed, 8 Dec 2021 22:32:41 +0100
Subject: ZofB_ne_correct unfinished

---
 lib/IEEE754_extra.v | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
index 56b90727..a0ae3089 100644
--- a/lib/IEEE754_extra.v
+++ b/lib/IEEE754_extra.v
@@ -1038,7 +1038,24 @@ Proof.
       apply Znearest_imp with (n := zm / p2p).
       apply Rabs_lt.
       split.
-      { admit. }
+      { assert (p2p > 0) as POS by lia.
+        pose proof (Z_mult_div_ge zm p2p POS).
+        assert (0 <= IZR zm * / IZR p2p - IZR (zm / p2p))%R.
+        2: lra.
+        assert (0 < IZR p2p)%R as POS2.
+        { apply IZR_lt. lia. }
+        field_simplify.
+        2: lra.
+        apply Rmult_le_pos.
+        { rewrite <- mult_IZR.
+          rewrite <- minus_IZR.
+          apply IZR_le.
+          lia.
+        }
+        assert (0 < / IZR p2p)%R.
+        2: lra.
+        apply Rinv_0_lt_compat. assumption.
+      }
       assert (0 < 2*(IZR p2p * IZR (zm / p2p) - IZR zm) + (IZR p2p))%R as LT.
       { rewrite <- mult_IZR.
         rewrite <- minus_IZR.
-- 
cgit