Relation between `set_seq` and `seq`.

46e116b9 · Robbert Krebbers · 5658dc85 · 46e116b9
Commit 46e116b9 authored Nov 30, 2018 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 4 additions and 0 deletions

theories/sets.v theories/sets.v +4 -0

No files found.
--- 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 *)