From b44bf4cb741eecc13dd147276bfe12cd4b856a2f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 9 Sep 2021 16:30:57 -0400
Subject: [PATCH] add size_set_seq
---
theories/fin_sets.v | 8 ++++++++
1 file changed, 8 insertions(+)
diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 14aef32f..62d089f7 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.
--
GitLab