diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 2e72335fb931f557ca533956df677b8fd97f1413..d53d3e05d58128e15b3f7075df126887a355c816 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -534,3 +534,11 @@ Section infinite.
   Qed.
 End infinite.
 End fin_set.
+
+Lemma size_set_seq `{FinSet nat C} start len :
+  size (set_seq (C:=C) start len) = len.
+Proof.
+  rewrite <-list_to_set_seq, size_list_to_set.
+  2:{ apply NoDup_seq. }
+  rewrite seq_length. done.
+Qed.