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.