From c5676b11618e7856ee296c3f498231603447088c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 11 Jan 2021 20:46:39 +0100
Subject: [PATCH] Shorten proof.

---
 theories/list_numbers.v | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index 2d8d2b3d..1bb5a816 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -80,11 +80,7 @@ Section seq.
 
   Lemma Forall_seq (P : nat → Prop) i n :
     Forall P (seq i n) ↔ ∀ j, i ≤ j < i + n → P j.
-  Proof.
-    rewrite Forall_lookup. split.
-    - intros H j [??]. apply (H (j - i)), lookup_seq. lia.
-    - intros H j x [-> ?]%lookup_seq. auto with lia.
-  Qed.
+  Proof. rewrite Forall_forall. setoid_rewrite elem_of_seq. auto with lia. Qed.
 End seq.
 
 (** ** Properties of the [seqZ] function *)
-- 
GitLab