one admit less

1 files changed, 20 insertions, 2 deletions

diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v
index fed327b7..5d1ce1ac 100644
--- a/kvx/FPDivision.v
+++ b/kvx/FPDivision.v
@@ -153,12 +153,13 @@ Proof.
     rewrite C1E.
     rewrite C0E.
     apply (Rabs_relax (bpow radix2 10)).
-    { cbn; lra. }
+    { apply bpow_lt; lia. }
     cbn.
     gappa.
   }
   change (is_finite 24 128 (BofZ 24 128 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) 1)) with true in C2F.
   destruct (C3 C2F) as (C3E & C3F & _).
+  clear C3.
   unfold Float.fma.
   assert (is_finite _ _ (Float.neg invb_d) = true) as invb_d_F.
   { Local Transparent Float.neg.
@@ -184,7 +185,24 @@ Proof.
           (Float.neg invb_d) b_d ExtFloat.one invb_d_F b_d_F one_F) as C5.
   
   rewrite Rlt_bool_true in C5; cycle 1.
-  { admit. }
+  { clear C5.
+    unfold Float.neg.
+    rewrite B2R_Bopp.
+    rewrite C3E.
+    rewrite C2E.
+    rewrite C0E.
+    rewrite C1E.
+    unfold ExtFloat.one.
+    change  (Float.of_int (Int.repr 1)) with (BofZ 53 1024 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) 1).
+    rewrite C9E.
+    unfold b_d.
+    rewrite Int64.unsigned_repr by lia.
+    rewrite C4E.
+    apply (Rabs_relax (bpow radix2 10)).
+    { apply bpow_lt; lia. }
+    cbn.
+    gappa.
+  }  
   destruct C5 as (C5E & C5F & _).
 
   pose proof (Bfma_correct 53 1024 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) Float.fma_nan mode_NE