progress in proof

1 files changed, 20 insertions, 3 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 424dfc77..a44de06e 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -184,9 +184,26 @@ Proof.
     fold b_d.
     set (r_invb_d := B2R 53 1024 invb_d) in *.
     set (r_b_d := B2R 53 1024 b_d) in *.
-    
-    unfold invb_d.
-    unfold invb_s.
     gappa.
   }
+  fold b_d in C6.
+  destruct C6 as (C6R & C6F & _).
+
+  pose proof (Bfma_correct 53 1024 re re Float.fma_nan mode_NE
+       (Bfma 53 1024 re re Float.fma_nan mode_NE
+          (Bopp 53 1024 Float.neg_nan invb_d) b_d (BofZ 53 1024 re re 1))
+       invb_d invb_d C6F C3F C3F) as C7.
+  rewrite Rlt_bool_true in C7; cycle 1.
+  { clear C7.
+    rewrite C6R.
+    rewrite B2R_Bopp.
+    eapply (Rabs_relax (bpow radix2 64)).
+    { apply bpow_lt. lia. }
+    rewrite C4R.
+    cbn.
+    set (r_invb_d := B2R 53 1024 invb_d) in *.
+    set (r_b_d := B2R 53 1024 b_d) in *.
+    gappa.
+  }
+  
 Admitted.