diff --git a/prelude/numbers.v b/prelude/numbers.v
index a9088d1f36955a0fc846975a48934f3698d1c354..6fc3ed36e8abd2e03e2a5eca67c5093adf31a545 100644
--- a/prelude/numbers.v
+++ b/prelude/numbers.v
@@ -3,7 +3,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 Eqdep PArith NArith ZArith NPeano.
+From Coq Require Export EqdepFacts PArith NArith ZArith NPeano.
 From Coq Require Import QArith Qcanon.
 From iris.prelude Require Export base decidable option.
 Open Scope nat_scope.