Reserve more notation in `integers.v`.

Avoid duplicating details like `at level 35`.

This is a bit of a slippery slope. (I reserved just the notation that
I overload elsewhere.)

theories/numbers.v

@@ -21,6 +21,12 @@ Reserved Notation "x < y < z" (at level 70, y at next level).
 Reserved Notation "x < y ≤ z" (at level 70, y at next level).
 Reserved Notation "x ≤ y ≤ z ≤ z'"
   (at level 70, y at next level, z at next level).
+Reserved Infix "`div`" (at level 35).
+Reserved Infix "`mod`" (at level 35).
+Reserved Infix "`quot`" (at level 35).
+Reserved Infix "`rem`" (at level 35).
+Reserved Infix "≪" (at level 35).
+Reserved Infix "≫" (at level 35).
 
 Infix "≤" := le : nat_scope.
 Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z)%nat : nat_scope.
@@ -30,8 +36,8 @@ Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z')%nat : nat_
 Notation "(≤)" := le (only parsing) : nat_scope.
 Notation "(<)" := lt (only parsing) : nat_scope.
 
-Infix "`div`" := Nat.div (at level 35) : nat_scope.
-Infix "`mod`" := Nat.modulo (at level 35) : nat_scope.
+Infix "`div`" := Nat.div : nat_scope.
+Infix "`mod`" := Nat.modulo : nat_scope.
 Infix "`max`" := Nat.max (at level 35) : nat_scope.
 Infix "`min`" := Nat.min (at level 35) : nat_scope.
 
@@ -213,8 +219,8 @@ Notation "x < y ≤ z" := (x < y ∧ y ≤ z)%N : N_scope.
 Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z')%N : N_scope.
 Notation "(≤)" := N.le (only parsing) : N_scope.
 Notation "(<)" := N.lt (only parsing) : N_scope.
-Infix "`div`" := N.div (at level 35) : N_scope.
-Infix "`mod`" := N.modulo (at level 35) : N_scope.
+Infix "`div`" := N.div : N_scope.
+Infix "`mod`" := N.modulo : N_scope.
 
 Arguments N.add : simpl never.
 
@@ -247,12 +253,12 @@ Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ 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.
-Infix "`quot`" := Z.quot (at level 35) : Z_scope.
-Infix "`rem`" := Z.rem (at level 35) : Z_scope.
-Infix "≪" := Z.shiftl (at level 35) : Z_scope.
-Infix "≫" := Z.shiftr (at level 35) : Z_scope.
+Infix "`div`" := Z.div : Z_scope.
+Infix "`mod`" := Z.modulo : Z_scope.
+Infix "`quot`" := Z.quot : Z_scope.
+Infix "`rem`" := Z.rem : Z_scope.
+Infix "≪" := Z.shiftl : Z_scope.
+Infix "≫" := Z.shiftr : Z_scope.
 
 Instance Zpos_inj : Inj (=) (=) Zpos.
 Proof. by injection 1. Qed.