diff --git a/theories/sets.v b/theories/sets.v
index 8b6d5768d965540cce20c56c139b9ab9d53b8914..23b28cf5bf783165a4a1b390d3a7bb09f94a08c3 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -1086,6 +1086,10 @@ Section set_seq.
   Lemma set_seq_S_end_union_L `{!LeibnizEquiv C} start len :
     set_seq start (S len) =@{C} {[ start + len ]} ∪ set_seq start len.
   Proof. unfold_leibniz. apply set_seq_S_end_union. Qed.
+
+  Lemma list_to_set_seq start len :
+    list_to_set (seq start len) =@{C} set_seq start len.
+  Proof. revert start; induction len; intros; f_equal/=; auto. Qed.
 End set_seq.
 
 (** Mimimal elements *)