Skip to content
Snippets Groups Projects
Commit c3bfb0b1 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'ralf/size_set_seq' into 'master'

add size_set_seq

See merge request !323
parents c5ee00e4 b44bf4cb
No related branches found
No related tags found
No related merge requests found
......@@ -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.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment