diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index f4116df156b0ed99b59856eab486c054aab85078..4a8b2af4fcfb92a5c817a0f7a523650082098fa8 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -67,7 +67,7 @@ Section seq.
   Qed.
   Lemma NoDup_seq j n : NoDup (seq j n).
   Proof. apply NoDup_ListNoDup, seq_NoDup. Qed.
-  Lemma seq_S_end_app j n : seq j (S n) = seq j n ++ [j + n].
+  Lemma seq_S_snoc j n : seq j (S n) = seq j n ++ [j + n].
   Proof.
     revert j. induction n as [|n IH]; intros j; simpl in *; f_equal; [done |].
     by rewrite IH, Nat.add_succ_r.