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.