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

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

diff --git a/stdpp/list_numbers.v b/stdpp/list_numbers.v
index 4d1b1b29..7e79e81d 100644
--- a/stdpp/list_numbers.v
+++ b/stdpp/list_numbers.v
@@ -98,10 +98,8 @@ Section seq.
     k ∈ seq j n ↔ j ≤ k < j + n.
   Proof. rewrite elem_of_list_In, in_seq. done. Qed.
 
-  Lemma seq_nil n m:
-  seq n m = [] ↔
-  m = 0.
-  Proof. by induction n; induction m. Qed.
+  Lemma seq_nil n m : seq n m = [] ↔ m = 0.
+  Proof. by destruct m. Qed.
 
   Lemma seq_subseteq m n1 n2 :
     n1 ≤ n2 →
-- 
GitLab