diff --git a/theories/normedtype_theory/num_normedtype.v b/theories/normedtype_theory/num_normedtype.v
index 91a7b37b92..d2f291e814 100644
--- a/theories/normedtype_theory/num_normedtype.v
+++ b/theories/normedtype_theory/num_normedtype.v
@@ -1,5 +1,4 @@
 (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
-From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix.
 From mathcomp Require Import rat interval zmodp vector fieldext falgebra.
 From mathcomp Require Import archimedean.