diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 14aef32f7ea7dfdca45fd550e907103ad6d04699..62d089f79e9066ab52dd611a7855ced9a2b327fc 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -523,3 +523,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.