From 794ce99ac2d17cdd50dd90b323d299ccbe0fe456 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 11 Jan 2021 18:50:32 +0100
Subject: [PATCH] add seqZ_S

---
 theories/list_numbers.v | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index b976599c..1caa8ede 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -156,6 +156,15 @@ Section seqZ.
     intros. simpl. lia.
   Qed.
 
+  Lemma seqZ_S m i : seqZ m (S i) = seqZ m i ++ [m + i].
+  Proof.
+    intros.
+    replace (Z.of_nat (S i)) with (Z.of_nat i + 1)%Z by lia.
+    rewrite seqZ_app; [|lia..].
+    unfold seqZ; simpl.
+    replace (0%nat + (m+i))%Z with (m + i)%Z by lia. done.
+  Qed.
+
   Lemma elem_of_seqZ m n k :
     k ∈ seqZ m n ↔ m ≤ k < m + n.
   Proof.
-- 
GitLab