diff --git a/lib/ModuRes/CBUltInst.v b/lib/ModuRes/CBUltInst.v
index b3547d422ca20d4cb7c9dca8ed9095f228a366e5..c1f896f7e180b925a94fe5bfd2ba60491b16d815 100644
--- a/lib/ModuRes/CBUltInst.v
+++ b/lib/ModuRes/CBUltInst.v
@@ -1,8 +1,8 @@
 (** This file provides the proof that CBUlt, the category of complete,
     bisected, ultrametric spaces, forms an M-category. *)
 
-Require Import MetricCore.
-Require Import MetricRec.
+Require Import CSetoid Constr.
+Require Import MetricCore MetricRec.
 
 Module CBUlt <: MCat.
   Local Open Scope cat_scope.
diff --git a/lib/ModuRes/Constr.v b/lib/ModuRes/Constr.v
index 5c3845a876147d87eb3d078826ecae8463b0e4c9..c6dce1e856cbdb47459d0c3f227bb08b7a8bd946 100644
--- a/lib/ModuRes/Constr.v
+++ b/lib/ModuRes/Constr.v
@@ -6,16 +6,9 @@
     - an extension operation on the space Tᵏ, for k ∈ nat, as a
       non-expansive morphism. *)
 
-Require Export UPred.
+Require Import UPred.
 Require Import MetricCore.
-Require Import Arith.
-
-Module NatDec.
-  Definition U := nat.
-  Definition eq_dec := eq_nat_dec.
-End NatDec.
-
-Module D := Coq.Logic.Eqdep_dec.DecidableEqDep(NatDec).
+Require Fin.
 
 Section Halving.
   Context (T : cmtyp).
@@ -174,8 +167,6 @@ Section EvaluationClosure.
 
 End EvaluationClosure.
 
-Require Fin.
-
 Definition transfer {A} {T : A -> Type} {x y : A} (EQ : x = y) (t : T x) : T y :=
   eq_rect x T t y EQ.
 
diff --git a/lib/ModuRes/MetricCore.v b/lib/ModuRes/MetricCore.v
index 5a4ec2dad4592963bf95b4ad0179c4929fa9240f..17d989b0b32152584f09ab6043b3f2fa5f8e1b4c 100644
--- a/lib/ModuRes/MetricCore.v
+++ b/lib/ModuRes/MetricCore.v
@@ -1001,3 +1001,11 @@ Section Option.
 End Option.
 
 Arguments dist {_ _ _} _ _ _ /.
+
+(* We have several users of this, so deifne it centrally *)
+Module NatDec.
+  Definition U := nat.
+  Definition eq_dec := eq_nat_dec.
+End NatDec.
+
+Module D := Coq.Logic.Eqdep_dec.DecidableEqDep(NatDec).