diff --git a/theories/collections.v b/theories/collections.v
index a650917f115b4f60e636b2a66dc136a469a5a29f..31c971ee84ff65ddeb02a93f33cc26a449062e2e 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -1053,6 +1053,10 @@ Section seq_set.
     - rewrite elem_of_union, elem_of_singleton, IH. omega.
   Qed.
 
+  Lemma seq_set_start_disjoint start len :
+    {[ start ]} ## seq_set (C:=C) (S start) len.
+  Proof. intros x. rewrite elem_of_singleton, elem_of_seq_set. omega. Qed.
+
   Lemma seq_set_S_disjoint start len :
     {[ start + len ]} ## seq_set (C:=C) start len.
   Proof. intros x. rewrite elem_of_singleton, elem_of_seq_set. omega. Qed.