diff --git a/stdpp/list_numbers.v b/stdpp/list_numbers.v
index 4d1b1b2970fca81230bd257d2260ef89007f24f9..7e79e81df7bfbb48b58c9d2c43892b30cae45f67 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 →