kvx/ExtIEEE754.v


1
2
3
4
5
6
7
8
9
10
11
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.