From dab5ceabe0b11daa0199a6a48c73adbee9fafb4c Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Thu, 16 Dec 2021 23:27:40 +0100
Subject: progress

---
 kvx/FPDivision.v | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v
index 6fd7e14c..1b81b632 100644
--- a/kvx/FPDivision.v
+++ b/kvx/FPDivision.v
@@ -435,11 +435,15 @@ Proof.
     gappa.
   }
 
+  assert(0 <= prod_r <= 4294967295) as prod_r_range.
+  { admit.
+  }
+
   replace (_ && _ ) with true; cycle 1.
   {
     symmetry.
     rewrite andb_true_iff.
-    admit.
+    split; apply Zle_imp_le_bool; lia.
   }
   cbn.
   f_equal.
-- 
cgit