From 0ca71551f9d47dcc04e7a97bb294a0379732bc04 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 14 Jan 2022 11:47:58 +0100
Subject: find_quotient

---
 kvx/FPDivision64.v | 24 +++++++++++++++++-------
 1 file changed, 17 insertions(+), 7 deletions(-)

(limited to 'kvx/FPDivision64.v')

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 6d82ae67..8f0d2fa1 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -1014,12 +1014,18 @@ Proof.
   
   pose proof (Zgt_cases (b * q) a)%Z as CASE.
   destruct (_ >? _)%Z.
-  { admit. }
-  apply Zdiv_unique with (b := (a - q*b)%Z).
-  ring.
+  { unfold b', q', a' in DELTA.
+    rewrite <- mult_IZR in DELTA.
+    rewrite <- minus_IZR in DELTA.
+    rewrite Rabs_Zabs in DELTA.
+    apply lt_IZR in DELTA.
+    rewrite Z.abs_eq in DELTA by lia.
+    
+    apply Zdiv_unique with (b := (a - (q-1)*b)%Z).
+    ring.
+    split; lia.
+  }
   
-  split.
-  { rewrite Z.mul_comm. lia. }
   rewrite <- Rabs_Ropp in DELTA.
   unfold b', q', a' in DELTA.
   rewrite <- mult_IZR in DELTA.
@@ -1028,8 +1034,12 @@ Proof.
   rewrite Rabs_Zabs in DELTA.
   apply lt_IZR in DELTA.
   rewrite Z.abs_eq in DELTA by lia.
-  lia.
-Admitted.
+
+  apply Zdiv_unique with (b := (a - q*b)%Z).
+  ring.
+  
+  split; lia.
+Qed.
 
 Definition step2_real_div_long a b :=
   Val.mulf (Val.maketotal (Val.floatoflong a)) (step1_real_inv_longu b).
-- 
cgit