remove singleoflongu (does not exist)

1 files changed, 22 insertions, 0 deletions

diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v
index 658bf0b3..e6cce0fa 100644
--- a/kvx/SelectOpproof.v
+++ b/kvx/SelectOpproof.v
@@ -1929,6 +1929,28 @@ Proof.
     }
     inv EVAL.
     constructor.
+  - cbn in *.
+    intro EVAL.
+    inv EVAL. discriminate.
+    inv H0. discriminate.
+    inv H2. 2: discriminate.
+    inv Heval.
+    intro EVAL.
+    destruct v1; try discriminate.
+    destruct v0; try discriminate.
+    unfold Int64.eq in EVAL.
+    change (Int64.unsigned Int64.zero) with 0 in EVAL.
+    unfold zeq in EVAL.
+    destruct (Z.eq_dec (Int64.unsigned i0) 0) as [EQ | NEQ].
+    { discriminate. }
+    exists (Vlong (Int64.divu i i0)). split.
+    {
+      apply FPDivision64.fp_divu64_correct; auto.
+      pose proof (Int64.unsigned_range i0).
+      lia.
+    }
+    inv EVAL.
+    constructor.
 Qed.
 
 End CMCONSTR.