diff --git a/tests/numbers.ref b/tests/numbers.ref
new file mode 100644
index 0000000000000000000000000000000000000000..8dd3efde5e3054ef29120bf0d328c4753761f23b
--- /dev/null
+++ b/tests/numbers.ref
@@ -0,0 +1,8 @@
+le
+     : nat → nat → Prop
+le
+     : nat → nat → Prop
+le
+     : nat → nat → Prop
+le
+     : nat → nat → Prop
diff --git a/tests/numbers.v b/tests/numbers.v
new file mode 100644
index 0000000000000000000000000000000000000000..3c8676c9c2369859501ce054d210f0359adbe85f
--- /dev/null
+++ b/tests/numbers.v
@@ -0,0 +1,22 @@
+From stdpp Require base numbers prelude.
+
+(** Check that we always get the [le] function on [nat]. *)
+Module test1.
+  Import stdpp.base.
+  Check le.
+End test1.
+
+Module test2.
+  Import stdpp.prelude.
+  Check le.
+End test2.
+
+Module test3.
+  Import stdpp.numbers.
+  Check le.
+End test3.
+
+Module test4.
+  Import stdpp.list.
+  Check le.
+End test4.
diff --git a/theories/base.v b/theories/base.v
index 7d63f1249391776006db679758172c8fd4b09307..a4cfdfb32ad72b913dae2f8b6ed1f556cf72e9f2 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -3,7 +3,7 @@ that are used throughout the whole development. Most importantly it contains
 abstract interfaces for ordered structures, sets, and various other data
 structures. *)
 
-From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
+From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid Arith.
 From Coq Require Import Permutation.
 Set Default Proof Using "Type".
 Export ListNotations.
diff --git a/theories/numbers.v b/theories/numbers.v
index d0b9d29d04566e1fda5cbc394844599dd5177f93..384977883ae3cd74afa07531bf99d0f6581f414b 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -1,7 +1,7 @@
 (** This file collects some trivial facts on the Coq types [nat] and [N] for
 natural numbers, and the type [Z] for integers. It also declares some useful
 notations. *)
-From Coq Require Export EqdepFacts PArith NArith ZArith NPeano.
+From Coq Require Export EqdepFacts PArith NArith ZArith Arith.
 From Coq Require Import QArith Qcanon.
 From stdpp Require Export base decidable option.
 Set Default Proof Using "Type".