From 3e2830ce5653f4142476e5380a46219cfac456d5 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Mon, 29 Jun 2026 20:55:11 +0900
Subject: [PATCH 1/6] reduce dep

---
 theories/measure_theory/measurable_function.v | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/theories/measure_theory/measurable_function.v b/theories/measure_theory/measurable_function.v
index 061d3b958c..ea845e68e5 100644
--- a/theories/measure_theory/measurable_function.v
+++ b/theories/measure_theory/measurable_function.v
@@ -1,11 +1,10 @@
 (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect_compat algebra.
+From mathcomp Require Import all_ssreflect_compat.
 #[warning="-warn-library-file-internal-analysis"]
 From mathcomp Require Import unstable.
-From mathcomp Require Import boolp classical_sets functions cardinality reals.
-From mathcomp Require Import ereal topology normedtype.
-From mathcomp Require Import sequences measurable_structure.
+From mathcomp Require Import boolp classical_sets functions.
+From mathcomp Require Import measurable_structure.
 
 (**md**************************************************************************)
 (* # Measurable Functions                                                     *)
@@ -29,7 +28,6 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 Import ProperNotations.
-Import Order.TTheory GRing.Theory Num.Theory.
 
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
@@ -358,7 +356,7 @@ Context {d} {T : measurableType d} {d1} {T1 : measurableType d1}
 
 Lemma g_sigma_algebra_preimage_comp (X : {mfun T >-> T1}) (f : T1 -> T2) :
   measurable_fun [set: T1] f ->
-  g_sigma_algebra_preimage (f \o X)%R `<=` g_sigma_algebra_preimage X.
+  g_sigma_algebra_preimage (f \o X) `<=` g_sigma_algebra_preimage X.
 Proof. exact: preimage_set_system_compS. Qed.
 
 End g_sigma_algebra_preimage_comp.

From e9c4b2ccfcc64ac93a0fb277049852f0f8d5a25c Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Tue, 30 Jun 2026 16:13:36 +0900
Subject: [PATCH 2/6] make normed module depends on metric

---
 .../normedtype_theory/matrix_normedtype.v     |  3 ++
 theories/normedtype_theory/normed_module.v    | 34 +++++++++++++++++--
 2 files changed, 34 insertions(+), 3 deletions(-)

diff --git a/theories/normedtype_theory/matrix_normedtype.v b/theories/normedtype_theory/matrix_normedtype.v
index 3cd89248c9..af82f8eaa1 100644
--- a/theories/normedtype_theory/matrix_normedtype.v
+++ b/theories/normedtype_theory/matrix_normedtype.v
@@ -251,6 +251,9 @@ HB.instance Definition _ (K : numFieldType) m n :=
   PseudoMetricNormedZmod_Lmodule_isNormedModule.Build K 'M[K]_(m, n)
     (@mx_normZ K m n).
 
+HB.instance Definition _ (K : numFieldType) m n :=
+  isNormedModule.Build _ 'M[K]_(m, n).
+
 End matrix_NormedModule.
 
 Lemma continuous_mx {V : topologicalType} {R : realFieldType} {m n : nat}
diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index c57a771abc..57ef3929aa 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -92,11 +92,33 @@ HB.mixin Record PseudoMetricNormedZmod_ConvexTvs_isNormedModule K V
   normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |;
 }.
 
-#[short(type="normedModType")]
-HB.structure Definition NormedModule (K : numDomainType) :=
+HB.structure Definition NormedModule0 (K : numDomainType) :=
   {T of PseudoMetricNormedZmod K T & ConvexTvs K T
    & PseudoMetricNormedZmod_ConvexTvs_isNormedModule K T}.
 
+#[short(type="normedModType")]
+HB.structure Definition NormedModule (K : numDomainType) :=
+  {T of NormedModule0 K T & Metric K T}.
+
+HB.factory Record isNormedModule (K : numDomainType) T of NormedModule0 K T := { }.
+
+HB.builders Context K T of isNormedModule K T.
+
+Let mdist (x y : T) : K := `|x - y|.
+
+Let mdist_ge0 x y : 0 <= mdist x y. Proof. by rewrite /mdist. Qed.
+
+Let mdist_positivity x y : mdist x y = 0 -> x = y.
+Proof. by move=> /normr0_eq0/subr0_eq. Qed.
+
+Let ballEmdist x d : ball x d = [set y | mdist x y < d].
+Proof. by rewrite -ball_normE. Qed.
+
+HB.instance Definition _ :=
+  @PseudoMetric_isMetric.Build K T mdist mdist_ge0 mdist_positivity ballEmdist.
+
+HB.end.
+
 #[short(type="subNormedModType")]
 HB.structure Definition SubNormedModule (R : numDomainType)
   (V : normedModType R) (S : pred V) :=
@@ -1721,7 +1743,7 @@ Qed.
 Section prod_NormedModule.
 Context {K : numFieldType} {U V : normedModType K}.
 
-Lemma prod_norm_scale (l : K) (x : U * V) : `| l *: x | = `|l| * `| x |.
+Let prod_norm_scale (l : K) (x : U * V) : `| l *: x | = `|l| * `| x |.
 Proof. by rewrite prod_normE /= !normrZ maxr_pMr. Qed.
 
 HB.instance Definition _ :=
@@ -1730,6 +1752,9 @@ HB.instance Definition _ :=
 
 End prod_NormedModule.
 
+HB.instance Definition _ (R : numFieldType) (U V' : normedModType R) :=
+  isNormedModule.Build _ (U * V')%type.
+
 Section prod_NormedModule_lemmas.
 Context {T : Type} {K : numDomainType} {U V : normedModType K}.
 
@@ -2657,6 +2682,9 @@ HB.instance Definition _ (V : vectType R) :=
   PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (max_space V)
     (@Norm.normZ _ _ (@max_norm V)).
 
+HB.instance Definition _ (V : vectType R) :=
+  isNormedModule.Build _ (max_space V).
+
 (* NB: Get Trocq to prove the continuity part automatically. *)
 Lemma sup_closed_ball_compact (V : vectType R) :
   compact (closed_ball (0 : max_space V) 1).

From 2cf3927216e17f8f9fab9e113b8dfb698de549e8 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Tue, 30 Jun 2026 19:01:36 +0900
Subject: [PATCH 3/6] fix

---
 theories/normedtype_theory/normed_module.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index 57ef3929aa..a6d9267c53 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -100,7 +100,7 @@ HB.structure Definition NormedModule0 (K : numDomainType) :=
 HB.structure Definition NormedModule (K : numDomainType) :=
   {T of NormedModule0 K T & Metric K T}.
 
-HB.factory Record isNormedModule (K : numDomainType) T of NormedModule0 K T := { }.
+HB.factory Record isNormedModule (K : numDomainType) T & NormedModule0 K T := { }.
 
 HB.builders Context K T of isNormedModule K T.
 

From 7f296d8d2b65a8296c349f3d2130e1024667e679 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Tue, 30 Jun 2026 21:12:05 +0900
Subject: [PATCH 4/6] fix

---
 theories/normedtype_theory/normed_module.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index a6d9267c53..7716dd3a5c 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -102,7 +102,7 @@ HB.structure Definition NormedModule (K : numDomainType) :=
 
 HB.factory Record isNormedModule (K : numDomainType) T & NormedModule0 K T := { }.
 
-HB.builders Context K T of isNormedModule K T.
+HB.builders Context K T & isNormedModule K T.
 
 Let mdist (x y : T) : K := `|x - y|.
 

From 0c6df76f415300b15360a0730444368b238ea41c Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Thu, 16 Jul 2026 17:02:30 +0900
Subject: [PATCH 5/6] gen to pseudoMetricNormedZmodule

---
 .../normedtype_theory/matrix_normedtype.v     |  6 +-
 theories/normedtype_theory/normed_module.v    | 55 +++++++++----------
 .../pseudometric_normed_Zmodule.v             | 45 ++++++++++++---
 3 files changed, 66 insertions(+), 40 deletions(-)

diff --git a/theories/normedtype_theory/matrix_normedtype.v b/theories/normedtype_theory/matrix_normedtype.v
index af82f8eaa1..18333a4238 100644
--- a/theories/normedtype_theory/matrix_normedtype.v
+++ b/theories/normedtype_theory/matrix_normedtype.v
@@ -219,6 +219,9 @@ HB.instance Definition _ :=
 
 End matrix_pseudoMetricNormedZmod.
 
+HB.instance Definition _ (K : numFieldType) m n :=
+  isPseudoMetricNormedZmod.Build _ 'M[K]_(m, n).
+
 Lemma bounded_closed_compact (R : realType) n (A : set 'rV[R]_n) :
   bounded_set A -> closed A -> compact A.
 Proof.
@@ -251,9 +254,6 @@ HB.instance Definition _ (K : numFieldType) m n :=
   PseudoMetricNormedZmod_Lmodule_isNormedModule.Build K 'M[K]_(m, n)
     (@mx_normZ K m n).
 
-HB.instance Definition _ (K : numFieldType) m n :=
-  isNormedModule.Build _ 'M[K]_(m, n).
-
 End matrix_NormedModule.
 
 Lemma continuous_mx {V : topologicalType} {R : realFieldType} {m n : nat}
diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index 7716dd3a5c..5accb12ee6 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -92,32 +92,10 @@ HB.mixin Record PseudoMetricNormedZmod_ConvexTvs_isNormedModule K V
   normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |;
 }.
 
-HB.structure Definition NormedModule0 (K : numDomainType) :=
-  {T of PseudoMetricNormedZmod K T & ConvexTvs K T
-   & PseudoMetricNormedZmod_ConvexTvs_isNormedModule K T}.
-
 #[short(type="normedModType")]
 HB.structure Definition NormedModule (K : numDomainType) :=
-  {T of NormedModule0 K T & Metric K T}.
-
-HB.factory Record isNormedModule (K : numDomainType) T & NormedModule0 K T := { }.
-
-HB.builders Context K T & isNormedModule K T.
-
-Let mdist (x y : T) : K := `|x - y|.
-
-Let mdist_ge0 x y : 0 <= mdist x y. Proof. by rewrite /mdist. Qed.
-
-Let mdist_positivity x y : mdist x y = 0 -> x = y.
-Proof. by move=> /normr0_eq0/subr0_eq. Qed.
-
-Let ballEmdist x d : ball x d = [set y | mdist x y < d].
-Proof. by rewrite -ball_normE. Qed.
-
-HB.instance Definition _ :=
-  @PseudoMetric_isMetric.Build K T mdist mdist_ge0 mdist_positivity ballEmdist.
-
-HB.end.
+  {T of PseudoMetricNormedZmod K T & ConvexTvs K T
+   & PseudoMetricNormedZmod_ConvexTvs_isNormedModule K T}.
 
 #[short(type="subNormedModType")]
 HB.structure Definition SubNormedModule (R : numDomainType)
@@ -391,6 +369,20 @@ HB.instance Definition _ := isPointed.Build M 0.
 
 HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R M erefl.
 
+(* TODO: why do we have to repeat this while we already have isPseudoMetricNormedZmod? *)
+Let mdist (x y : M) : R := `|x - y|.
+
+Let mdist_ge0 x y : 0 <= mdist x y. Proof. by rewrite /mdist. Qed.
+
+Let mdist_positivity x y : mdist x y = 0 -> x = y.
+Proof. by move=> /normr0_eq0/subr0_eq. Qed.
+
+Let ballEmdist x d : ball x d = [set y | mdist x y < d].
+Proof. by rewrite -ball_normE. Qed.
+
+HB.instance Definition _ :=
+  @PseudoMetric_isMetric.Build R M mdist mdist_ge0 mdist_positivity ballEmdist.
+
 HB.instance Definition _ :=
   PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R M normrZ.
 
@@ -1740,6 +1732,10 @@ apply/connected_intervalP/connected_continuous_connected => //.
 exact: segment_connected.
 Qed.
 
+(* TODO: move to pseudometric_normed_Zmodule.v *)
+HB.instance Definition _ (R : numDomainType) (U V' : pseudoMetricNormedZmodType R) :=
+  isPseudoMetricNormedZmod.Build _ (U * V')%type.
+
 Section prod_NormedModule.
 Context {K : numFieldType} {U V : normedModType K}.
 
@@ -1753,10 +1749,11 @@ HB.instance Definition _ :=
 End prod_NormedModule.
 
 HB.instance Definition _ (R : numFieldType) (U V' : normedModType R) :=
-  isNormedModule.Build _ (U * V')%type.
+  NormedModule.on (U * V')%type.
 
+(* TODO: move to pseudometric_normed_Zmodule.v *)
 Section prod_NormedModule_lemmas.
-Context {T : Type} {K : numDomainType} {U V : normedModType K}.
+Context {T : Type} {K : numDomainType} {U V : pseudoMetricNormedZmodType K}.
 
 Lemma fcvgr2dist_ltP {F : set_system U} {G : set_system V}
   {FF : Filter F} {FG : Filter G} (y : U) (z : V) :
@@ -2679,11 +2676,11 @@ HB.instance Definition _ (V : vectType R) :=
   NormedZmod_PseudoMetric_eq.Build R (max_space V) erefl.
 
 HB.instance Definition _ (V : vectType R) :=
-  PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (max_space V)
-    (@Norm.normZ _ _ (@max_norm V)).
+  isPseudoMetricNormedZmod.Build _ (max_space V).
 
 HB.instance Definition _ (V : vectType R) :=
-  isNormedModule.Build _ (max_space V).
+  PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (max_space V)
+    (@Norm.normZ _ _ (@max_norm V)).
 
 (* NB: Get Trocq to prove the continuity part automatically. *)
 Lemma sup_closed_ball_compact (V : vectType R) :
diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
index 9f945624de..713efff73c 100644
--- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v
+++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
@@ -148,11 +148,45 @@ HB.mixin Record NormedZmod_PseudoMetric_eq (R : numDomainType) T
   pseudo_metric_ball_norm : ball = ball_ (fun x : T => `| x |)
 }.
 
-#[short(type="pseudoMetricNormedZmodType")]
-HB.structure Definition PseudoMetricNormedZmod (R : numDomainType) :=
+HB.structure Definition PseudoMetricNormedZmod0 (R : numDomainType) :=
   {T of Num.NormedZmodule R T & PseudoMetric R T
    & NormedZmod_PseudoMetric_eq R T & isPointed T}.
 
+#[short(type="pseudoMetricNormedZmodType")]
+HB.structure Definition PseudoMetricNormedZmod (R : numDomainType) :=
+  {T of PseudoMetricNormedZmod0 R T & Metric R T}.
+
+Section pseudoMetricNormedZmod_numDomainType.
+Context {K : numDomainType} {V : PseudoMetricNormedZmod0.type K}.
+
+(**md Balls defined by the norm: *)
+Local Notation ball_norm := (ball_ (@Num.norm K V)).
+
+Lemma ball_normE : ball_norm = ball.
+Proof. by rewrite pseudo_metric_ball_norm. Qed.
+
+End pseudoMetricNormedZmod_numDomainType.
+
+HB.factory Record isPseudoMetricNormedZmod
+  (K : numDomainType) T & PseudoMetricNormedZmod0 K T := { }.
+
+HB.builders Context K T & isPseudoMetricNormedZmod K T.
+
+Let mdist (x y : T) : K := `|x - y|.
+
+Let mdist_ge0 x y : 0 <= mdist x y. Proof. by rewrite /mdist. Qed.
+
+Let mdist_positivity x y : mdist x y = 0 -> x = y.
+Proof. by move=> /normr0_eq0/subr0_eq. Qed.
+
+Let ballEmdist x d : ball x d = [set y | mdist x y < d].
+Proof. by rewrite -ball_normE. Qed.
+
+HB.instance Definition _ :=
+  @PseudoMetric_isMetric.Build K T mdist mdist_ge0 mdist_positivity ballEmdist.
+
+HB.end.
+
 (* alternative definition of a PseudoMetricNormedZmod *)
 HB.factory Record NormedZmoduleMetric (R : numDomainType) T
     & Num.NormedZmodule R T & Metric R T & isPointed T := {
@@ -175,12 +209,6 @@ HB.end.
 Section pseudoMetricNormedZmod_numDomainType.
 Context {K : numDomainType} {V : pseudoMetricNormedZmodType K}.
 
-(**md Balls defined by the norm: *)
-Local Notation ball_norm := (ball_ (@Num.norm K V)).
-
-Lemma ball_normE : ball_norm = ball.
-Proof. by rewrite pseudo_metric_ball_norm. Qed.
-
 Lemma ball_open (x : V) (r : K) : open (ball x r).
 Proof.
 rewrite openE/= -ball_normE/= /interior => y /= bxy; rewrite -nbhs_ballE.
@@ -193,6 +221,7 @@ Lemma ball_open_nbhs (x : V) (r : K) : 0 < r -> open_nbhs x (ball x r).
 Proof. by move=> e0; split; [exact: ball_open|exact: ballxx]. Qed.
 
 (**md Neighborhoods defined by the norm: *)
+Local Notation ball_norm := (ball_ (@Num.norm K V)).
 Local Notation nbhs_norm := (nbhs_ball_ ball_norm).
 
 (* if we do not give the V argument to nbhs, the universally quantified set that

From ce411225de7b06eef108fa5debe355a56622d89d Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Sun, 19 Jul 2026 18:51:22 +0900
Subject: [PATCH 6/6] changelog and doc

---
 CHANGELOG_UNRELEASED.md                       | 16 +++--
 .../normedtype_theory/matrix_normedtype.v     |  5 +-
 theories/normedtype_theory/normed_module.v    | 57 +-----------------
 .../pseudometric_normed_Zmodule.v             | 58 +++++++++++++++----
 4 files changed, 61 insertions(+), 75 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index cdb5e9c229..43d72fb6ab 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -186,12 +186,6 @@
   + lemma `ge0_integration_by_substitution_shift_itvy`,
     `ge0_integration_by_substitution_shift_itvNy`
 
-### Changed
-
-- moved from `measurable_structure.v` to `classical_sets.v`:
-  + definition `preimage_set_system`
-  + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`,
-    `preimage_set_system_id`
 - in `functions.v`:
   + lemmas `linfunP`, `linfun_eqP`
   + instances of `SubLmodule` and `pointedType` on `{linear _->_ | _ }`
@@ -224,6 +218,10 @@
 - in `realsum.v`:
   + lemma `__admitted__psumB` proved and renamed to `psumB`
 
+- in `pseudometric_normed_Zmodule.v`:
+  + factory `isPseudoMetricNormedZmodule`
+  + structure `PseudoMetricNormedZmod0`
+
 ### Changed
 
 - moved from `measurable_structure.v` to `classical_sets.v`:
@@ -335,6 +333,12 @@
   + definition `seqD`
   + lemmas `eq_bigcup_seqD`, `trivIset_seqD`, `seqDU_seqD`, `bigcup_bigsetU_bigcup`
 
+- in `pseudometric_normed_Zmodule.v`:
+  + structure `PseudoMetricNormedZmod` not inherits from `Metric`
+
+- moved form `normed_module.v` to `pseudometric_normed_Zmodule.v` and generalized:
+  + lemmas `fcvgr2dist_ltP`, `cvgr2dist_ltP`, `cvgr2dist_lt`
+
 ### Renamed
 
 - in `tvs.v`:
diff --git a/theories/normedtype_theory/matrix_normedtype.v b/theories/normedtype_theory/matrix_normedtype.v
index 18333a4238..21712108a2 100644
--- a/theories/normedtype_theory/matrix_normedtype.v
+++ b/theories/normedtype_theory/matrix_normedtype.v
@@ -217,10 +217,9 @@ Qed.
 HB.instance Definition _ :=
   NormedZmod_PseudoMetric_eq.Build K 'M[K]_(m, n) mx_norm_ball.
 
-End matrix_pseudoMetricNormedZmod.
+HB.instance Definition _ := isPseudoMetricNormedZmodule.Build _ 'M[K]_(m, n).
 
-HB.instance Definition _ (K : numFieldType) m n :=
-  isPseudoMetricNormedZmod.Build _ 'M[K]_(m, n).
+End matrix_pseudoMetricNormedZmod.
 
 Lemma bounded_closed_compact (R : realType) n (A : set 'rV[R]_n) :
   bounded_set A -> closed A -> compact A.
diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index 5accb12ee6..f193ea6aaf 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -369,19 +369,7 @@ HB.instance Definition _ := isPointed.Build M 0.
 
 HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R M erefl.
 
-(* TODO: why do we have to repeat this while we already have isPseudoMetricNormedZmod? *)
-Let mdist (x y : M) : R := `|x - y|.
-
-Let mdist_ge0 x y : 0 <= mdist x y. Proof. by rewrite /mdist. Qed.
-
-Let mdist_positivity x y : mdist x y = 0 -> x = y.
-Proof. by move=> /normr0_eq0/subr0_eq. Qed.
-
-Let ballEmdist x d : ball x d = [set y | mdist x y < d].
-Proof. by rewrite -ball_normE. Qed.
-
-HB.instance Definition _ :=
-  @PseudoMetric_isMetric.Build R M mdist mdist_ge0 mdist_positivity ballEmdist.
+HB.instance Definition _ := isPseudoMetricNormedZmodule.Build R M.
 
 HB.instance Definition _ :=
   PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R M normrZ.
@@ -389,7 +377,7 @@ HB.instance Definition _ :=
 HB.end.
 
 Definition subLmodule_isSubNormedmodule (R : realFieldType)
-    (V : normedModType R) (S : pred V) (U : Type) : Type := U.
+  (V : normedModType R) (S : pred V) (U : Type) : Type := U.
 
 Section SubLmodule_isSubNormedmodule.
 Context (R : realFieldType) (V : normedModType R) (S : pred V)
@@ -1732,10 +1720,6 @@ apply/connected_intervalP/connected_continuous_connected => //.
 exact: segment_connected.
 Qed.
 
-(* TODO: move to pseudometric_normed_Zmodule.v *)
-HB.instance Definition _ (R : numDomainType) (U V' : pseudoMetricNormedZmodType R) :=
-  isPseudoMetricNormedZmod.Build _ (U * V')%type.
-
 Section prod_NormedModule.
 Context {K : numFieldType} {U V : normedModType K}.
 
@@ -1748,41 +1732,6 @@ HB.instance Definition _ :=
 
 End prod_NormedModule.
 
-HB.instance Definition _ (R : numFieldType) (U V' : normedModType R) :=
-  NormedModule.on (U * V')%type.
-
-(* TODO: move to pseudometric_normed_Zmodule.v *)
-Section prod_NormedModule_lemmas.
-Context {T : Type} {K : numDomainType} {U V : pseudoMetricNormedZmodType K}.
-
-Lemma fcvgr2dist_ltP {F : set_system U} {G : set_system V}
-  {FF : Filter F} {FG : Filter G} (y : U) (z : V) :
-  (F, G) --> (y, z) <->
-  forall eps, 0 < eps ->
-   \forall y' \near F & z' \near G, `| (y, z) - (y', z') | < eps.
-Proof. exact: fcvgrPdist_lt. Qed.
-
-Lemma cvgr2dist_ltP {I J} {F : set_system I} {G : set_system J}
-  {FF : Filter F} {FG : Filter G} (f : I -> U) (g : J -> V) (y : U) (z : V) :
-  (f @ F, g @ G) --> (y, z) <->
-  forall eps, 0 < eps ->
-   \forall i \near F & j \near G, `| (y, z) - (f i, g j) | < eps.
-Proof.
-rewrite fcvgr2dist_ltP; split=> + e e0 => /(_ e e0);
-  by rewrite !near_simpl// => ?; rewrite !near_simpl.
-Qed.
-
-Lemma cvgr2dist_lt {I J} {F : set_system I} {G : set_system J}
-  {FF : Filter F} {FG : Filter G} (f : I -> U) (g : J -> V) (y : U) (z : V) :
-  (f @ F, g @ G) --> (y, z) ->
-  forall eps, 0 < eps ->
-   \forall i \near F & j \near G, `| (y, z) - (f i, g j) | < eps.
-Proof. by rewrite cvgr2dist_ltP. Qed.
-
-End prod_NormedModule_lemmas.
-Arguments cvgr2dist_ltP {_ _ _ _ _ F G FF FG}.
-Arguments cvgr2dist_lt {_ _ _ _ _ F G FF FG}.
-
 (* Local properties in R *)
 
 (* Topology on [R]² *)
@@ -2676,7 +2625,7 @@ HB.instance Definition _ (V : vectType R) :=
   NormedZmod_PseudoMetric_eq.Build R (max_space V) erefl.
 
 HB.instance Definition _ (V : vectType R) :=
-  isPseudoMetricNormedZmod.Build _ (max_space V).
+  isPseudoMetricNormedZmodule.Build _ (max_space V).
 
 HB.instance Definition _ (V : vectType R) :=
   PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (max_space V)
diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
index 713efff73c..4236fa6b3b 100644
--- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v
+++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
@@ -29,8 +29,9 @@ From mathcomp Require Import prodnormedzmodule num_normedtype.
 (*                                                                            *)
 (* ## Normed topological abelian groups                                       *)
 (* ```                                                                        *)
-(*  pseudoMetricNormedZmodType R == interface type for a normed topological   *)
+(*     PseudoMetricNormedZmod0 R == interface type for a normed topological   *)
 (*                                  abelian group equipped with a norm        *)
+(*  pseudoMetricNormedZmodType R == PseudoMetricNormedZmod0 R + Metric R      *)
 (*                                  The HB class is PseudoMetricNormedZmod.   *)
 (*           NormedZmoduleMetric == factory for pseudoMetricNormedZmodType    *)
 (*                                  based on metric structures                *)
@@ -149,14 +150,10 @@ HB.mixin Record NormedZmod_PseudoMetric_eq (R : numDomainType) T
 }.
 
 HB.structure Definition PseudoMetricNormedZmod0 (R : numDomainType) :=
-  {T of Num.NormedZmodule R T & PseudoMetric R T
-   & NormedZmod_PseudoMetric_eq R T & isPointed T}.
+  {T of Num.NormedZmodule R T & PseudoPointedMetric R T
+   & NormedZmod_PseudoMetric_eq R T }.
 
-#[short(type="pseudoMetricNormedZmodType")]
-HB.structure Definition PseudoMetricNormedZmod (R : numDomainType) :=
-  {T of PseudoMetricNormedZmod0 R T & Metric R T}.
-
-Section pseudoMetricNormedZmod_numDomainType.
+Section PseudoMetricNormedZmod0_numDomainType.
 Context {K : numDomainType} {V : PseudoMetricNormedZmod0.type K}.
 
 (**md Balls defined by the norm: *)
@@ -165,12 +162,16 @@ Local Notation ball_norm := (ball_ (@Num.norm K V)).
 Lemma ball_normE : ball_norm = ball.
 Proof. by rewrite pseudo_metric_ball_norm. Qed.
 
-End pseudoMetricNormedZmod_numDomainType.
+End PseudoMetricNormedZmod0_numDomainType.
+
+#[short(type="pseudoMetricNormedZmodType")]
+HB.structure Definition PseudoMetricNormedZmod (R : numDomainType) :=
+  {T of PseudoMetricNormedZmod0 R T & Metric R T}.
 
-HB.factory Record isPseudoMetricNormedZmod
+HB.factory Record isPseudoMetricNormedZmodule
   (K : numDomainType) T & PseudoMetricNormedZmod0 K T := { }.
 
-HB.builders Context K T & isPseudoMetricNormedZmod K T.
+HB.builders Context K T & isPseudoMetricNormedZmodule K T.
 
 Let mdist (x y : T) : K := `|x - y|.
 
@@ -498,14 +499,47 @@ rewrite /ball /= /prod_ball -!ball_normE /ball_ /=.
 by rewrite comparable_gt_max// ?real_comparable//; split=> /andP.
 Qed.
 
-Lemma prod_norm_ball : @ball _ (U * V)%type = ball_ (fun x => `|x|).
+Let prod_norm_ball : @ball _ (U * V)%type = ball_ (fun x => `|x|).
 Proof. by rewrite /= - ball_prod_normE. Qed.
 
 HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build K (U * V)%type
   prod_norm_ball.
 
+HB.instance Definition _ := isPseudoMetricNormedZmodule.Build _ (U * V)%type.
+
 End prod_pseudoMetricNormedZmod.
 
+Section prod_NormedModule_lemmas.
+Context {T : Type} {K : numDomainType} {U V : pseudoMetricNormedZmodType K}.
+
+Lemma fcvgr2dist_ltP {F : set_system U} {G : set_system V}
+  {FF : Filter F} {FG : Filter G} (y : U) (z : V) :
+  (F, G) --> (y, z) <->
+  forall eps, 0 < eps ->
+   \forall y' \near F & z' \near G, `| (y, z) - (y', z') | < eps.
+Proof. exact: fcvgrPdist_lt. Qed.
+
+Lemma cvgr2dist_ltP {I J} {F : set_system I} {G : set_system J}
+  {FF : Filter F} {FG : Filter G} (f : I -> U) (g : J -> V) (y : U) (z : V) :
+  (f @ F, g @ G) --> (y, z) <->
+  forall eps, 0 < eps ->
+   \forall i \near F & j \near G, `| (y, z) - (f i, g j) | < eps.
+Proof.
+rewrite fcvgr2dist_ltP; split=> + e e0 => /(_ e e0);
+  by rewrite !near_simpl// => ?; rewrite !near_simpl.
+Qed.
+
+Lemma cvgr2dist_lt {I J} {F : set_system I} {G : set_system J}
+  {FF : Filter F} {FG : Filter G} (f : I -> U) (g : J -> V) (y : U) (z : V) :
+  (f @ F, g @ G) --> (y, z) ->
+  forall eps, 0 < eps ->
+   \forall i \near F & j \near G, `| (y, z) - (f i, g j) | < eps.
+Proof. by rewrite cvgr2dist_ltP. Qed.
+
+End prod_NormedModule_lemmas.
+Arguments cvgr2dist_ltP {_ _ _ _ _ F G FF FG}.
+Arguments cvgr2dist_lt {_ _ _ _ _ F G FF FG}.
+
 Section standard_topology_pseudoMetricNormedZmod.
 Variable R : numFieldType.