diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index 2d8d2b3ddeec4d951d104b2b1ba158349ff230a2..1bb5a81625c3f0c29748a41af9b9b4165701f3f0 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 *)