diff --git a/src/elementary-number-theory/decreasing-sequences-natural-numbers.lagda.md b/src/elementary-number-theory/decreasing-sequences-natural-numbers.lagda.md
index c0af103770..4ef89df848 100644
--- a/src/elementary-number-theory/decreasing-sequences-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/decreasing-sequences-natural-numbers.lagda.md
@@ -80,9 +80,9 @@ module _
   {f : sequence ℕ} (H : is-decreasing-sequence-ℕ f)
   where
 
-  is-∞-zero-value-is-zero-value-decreasing-sequence-ℕ :
+  ∞-zero-value-is-zero-value-decreasing-sequence-ℕ :
     Σ ℕ (is-value-sequence zero-ℕ f) → is-∞-value-sequence zero-ℕ f
-  is-∞-zero-value-is-zero-value-decreasing-sequence-ℕ =
+  ∞-zero-value-is-zero-value-decreasing-sequence-ℕ =
     tot
       ( λ n K k I →
         is-zero-leq-zero-ℕ'