diff --git a/theories/normedtype.v b/theories/normedtype.v
index d8ae31c1a1..462bf0a3e1 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -2406,14 +2406,6 @@ Qed.
 (** Continuity of norm *)
 End NVS_continuity_normedModType.
 
-Lemma regular_Uniform_isEvt (R : numFieldType) : Uniform_isEvt R R^o.
-Proof.
-split.
-
-Search "cont" (GRing.add).
-
-
-
 Section NVS_continuity_mul.
 
 Context {K : numFieldType}.