Library Coq.ZArith.ZOdiv_def

Require Import BinInt.

Notation ZOdiv_eucl := Z.quotrem (only parsing).
Notation ZOdiv := Z.quot (only parsing).
Notation ZOmod := Z.rem (only parsing).

Notation ZOdiv_eucl_correct := Z.quotrem_eq.