diff --git a/theories/numbers.v b/theories/numbers.v
index 420bf69080ca923a810df34f24c28de39d1a6f27..c4198fefa7ea175d2bd269771f7837cc8956ea6f 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -88,6 +88,9 @@ Notation "x < y ≤ z" := (x < y ∧ y ≤ z)%Z : Z_scope.
 Notation "(≤)" := Z.le (only parsing) : Z_scope.
 Notation "(<)" := Z.lt (only parsing) : Z_scope.
 
+Infix "`div`" := Z.div (at level 35) : Z_scope.
+Infix "`mod`" := Z.modulo (at level 35) : Z_scope.
+
 Instance Z_eq_dec: ∀ x y : Z, Decision (x = y) := Z.eq_dec.
 Instance Z_le_dec: ∀ x y : Z, Decision (x ≤ y)%Z := Z_le_dec.
 Instance Z_lt_dec: ∀ x y : Z, Decision (x < y)%Z := Z_lt_dec.