proposition: Lemma size_set_seq `{FinSet nat C} start len : size (set_seq (C:=C) start len) = len.
proof: Proof. rewrite <-list_to_set_seq, size_list_to_set. 2:{ apply NoDup_seq. } rewrite seq_length. done. Qed.
imports: stdpp(relations) stdpp(options)