From 17deaa934be5290eb8d9df643a4e09d6994e660d Mon Sep 17 00:00:00 2001
From: malarbol <malarbol+git@gmail.com>
Date: Thu, 13 Jun 2024 18:39:13 +0200
Subject: [PATCH] cleanup

---
 .../decreasing-sequences-natural-numbers.lagda.md             | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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-ℕ'