diff --git a/reals/fast/CRexp.v b/reals/fast/CRexp.v
index 6ccdfbf3..89936c3e 100644
--- a/reals/fast/CRexp.v
+++ b/reals/fast/CRexp.v
@@ -36,7 +36,6 @@ Require Import CoRN.reals.fast.CRpower.
 Require Import CoRN.transc.Exponential.
 Require Import CoRN.transc.RealPowers.
 Require Import CoRN.reals.fast.Compress.
-Require Import Coq.NArith.Ndigits.
 Require Import CoRN.reals.fast.ModulusDerivative.
 Require Import CoRN.reals.fast.ContinuousCorrect.
 Require Import CoRN.reals.fast.CRsign.
diff --git a/reals/fast/CRroot.v b/reals/fast/CRroot.v
index e3c91c97..91008703 100644
--- a/reals/fast/CRroot.v
+++ b/reals/fast/CRroot.v
@@ -33,7 +33,6 @@ Require Import CoRN.model.metric2.Qmetric.
 Require Import Coq.QArith.Qpower.
 Require Import CoRN.model.ordfields.Qordfield.
 Require Import CoRN.reals.fast.Compress.
-Require Import Coq.NArith.Ndigits.
 Require Import CoRN.reals.fast.PowerBound.
 Require Import CoRN.transc.RealPowers.
 Require Import CoRN.reals.fast.ContinuousCorrect.
diff --git a/reals/fast/CRsin.v b/reals/fast/CRsin.v
index b70febb4..b4aa2876 100644
--- a/reals/fast/CRsin.v
+++ b/reals/fast/CRsin.v
@@ -39,7 +39,6 @@ Require Import CoRN.reals.fast.ContinuousCorrect.
 Require Import CoRN.model.metric2.Qmetric.
 Require Import CoRN.transc.PowerSeries.
 Require Import CoRN.transc.SinCos.
-Require Import Coq.NArith.Ndigits.
 Require Import CoRN.reals.fast.Compress.
 Require Import CoRN.reals.fast.PowerBound.
 Require Import CoRN.tactics.CornTac.
diff --git a/reals/fast/PowerBound.v b/reals/fast/PowerBound.v
index 028f6c2e..4789d743 100644
--- a/reals/fast/PowerBound.v
+++ b/reals/fast/PowerBound.v
@@ -22,7 +22,6 @@ CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
 Require Import CoRN.algebra.RSetoid.
 Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.UniformContinuity.
-Require Import Coq.NArith.Ndigits.
 Require Import Coq.ZArith.ZArith.
 Require Import Coq.Program.Basics.
 Require Import Coq.QArith.Qpower.