From a91677691b980d0c59c8638e5b83ba7fd7debb68 Mon Sep 17 00:00:00 2001
From: Kimaya Bedarkar <kbedarka@mpi-sws.org>
Date: Thu, 20 Feb 2025 09:33:56 +0000
Subject: [PATCH] Apply 1 suggestion(s) to 1 file(s)

Co-authored-by: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
---
 stdpp/list_numbers.v | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/stdpp/list_numbers.v b/stdpp/list_numbers.v
index 7e79e81d..4489e5a8 100644
--- a/stdpp/list_numbers.v
+++ b/stdpp/list_numbers.v
@@ -101,9 +101,7 @@ Section seq.
   Lemma seq_nil n m : seq n m = [] ↔ m = 0.
   Proof. by destruct m. Qed.
 
-  Lemma seq_subseteq m n1 n2 :
-    n1 ≤ n2 →
-    seq m n1 ⊆ seq m n2.
+  Lemma seq_subseteq_mono m n1 n2 : n1 ≤ n2 → seq m n1 ⊆ seq m n2.
   Proof. by intros Hle i Hi%elem_of_seq; apply elem_of_seq; lia. Qed.
 
   Lemma Forall_seq (P : nat → Prop) i n :
-- 
GitLab