diff --git a/stdpp/list_numbers.v b/stdpp/list_numbers.v
index 7e79e81df7bfbb48b58c9d2c43892b30cae45f67..4489e5a89e7876c5e870e3292adcdd0f2a9748ae 100644
--- a/stdpp/list_numbers.v
+++ b/stdpp/list_numbers.v
@@ -101,9 +101,7 @@ Section seq.
   Lemma seq_nil n m : seq n m = [] ↔ m = 0.
   Proof. by destruct m. Qed.
 
-  Lemma seq_subseteq m n1 n2 :
-    n1 ≤ n2 →
-    seq m n1 ⊆ seq m n2.
+  Lemma seq_subseteq_mono m n1 n2 : n1 ≤ n2 → seq m n1 ⊆ seq m n2.
   Proof. by intros Hle i Hi%elem_of_seq; apply elem_of_seq; lia. Qed.
 
   Lemma Forall_seq (P : nat → Prop) i n :