diff --git a/stdpp/numbers.v b/stdpp/numbers.v
index a9427ae880ec620b08675b95d3f0cad39a720cd9..8e653c9950115c53e565b1a7f09e9a61f4229e19 100644
--- a/stdpp/numbers.v
+++ b/stdpp/numbers.v
@@ -355,28 +355,32 @@ Infix "`min`" := N.min (at level 35) : N_scope.
 
 Global Arguments N.add : simpl never.
 
-Global Instance Npos_inj : Inj (=) (=) Npos.
-Proof. by injection 1. Qed.
+Global Hint Extern 0 (_ ≤ _)%N => reflexivity : core.
 
-Global Instance N_eq_dec: EqDecision N := N.eq_dec.
-Global Program Instance N_le_dec : RelDecision N.le := λ x y,
-  match N.compare x y with Gt => right _ | _ => left _ end.
-Solve Obligations with naive_solver.
-Global Program Instance N_lt_dec : RelDecision N.lt := λ x y,
-  match N.compare x y with Lt => left _ | _ => right _ end.
-Solve Obligations with naive_solver.
-Global Instance N_inhabited: Inhabited N := populate 1%N.
-Global Instance N_lt_pi x y : ProofIrrel (x < y)%N.
-Proof. unfold N.lt. apply _. Qed.
-
-Global Instance N_le_po: PartialOrder (≤)%N.
-Proof.
-  repeat split; red; [apply N.le_refl | apply N.le_trans | apply N.le_antisymm].
-Qed.
-Global Instance N_le_total: Total (≤)%N.
-Proof. repeat intro; lia. Qed.
+Module N.
+  Export BinNat.N.
 
-Global Hint Extern 0 (_ ≤ _)%N => reflexivity : core.
+  Global Instance pos_inj : Inj (=) (=) N.pos.
+  Proof. by injection 1. Qed.
+
+  Global Instance eq_dec : EqDecision N := N.eq_dec.
+  Global Program Instance le_dec : RelDecision N.le := λ x y,
+    match N.compare x y with Gt => right _ | _ => left _ end.
+  Solve Obligations with naive_solver.
+  Global Program Instance lt_dec : RelDecision N.lt := λ x y,
+    match N.compare x y with Lt => left _ | _ => right _ end.
+  Solve Obligations with naive_solver.
+  Global Instance inhabited : Inhabited N := populate 1%N.
+  Global Instance lt_pi x y : ProofIrrel (x < y)%N.
+  Proof. unfold N.lt. apply _. Qed.
+
+  Global Instance le_po : PartialOrder (≤)%N.
+  Proof.
+    repeat split; red; [apply N.le_refl | apply N.le_trans | apply N.le_antisymm].
+  Qed.
+  Global Instance le_total : Total (≤)%N.
+  Proof. repeat intro; lia. Qed.
+End N.
 
 (** * Notations and properties of [Z] *)
 Local Open Scope Z_scope.