1 files changed, 12 insertions, 0 deletions
diff --git a/kvx/ExtIEEE754.v b/kvx/ExtIEEE754.v
new file mode 100644
index 00000000..095fd0cc
--- /dev/null
+++ b/kvx/ExtIEEE754.v
@@ -0,0 +1,12 @@
+Require Import Coq.ZArith.Zdiv.
+
+Open Scope Z.
+
+Definition Zdiv_ne (a b : Z) :=
+  let q := Z.div a b in
+  let q1 := Z.succ q in
+  match Z.compare (a-b*q) (b*q1-a) with
+  | Lt => q
+  | Gt => q1
+  | Eq => (if Z.even q then q else q1)
+  end.