proposition: Lemma elem_of_set_seq start len x : x ∈ set_seq (C:=C) start len ↔ start ≤ x < start + len.
proof: Proof. revert start. induction len as [|len IH]; intros start; simpl. - rewrite elem_of_empty. lia. - rewrite elem_of_union, elem_of_singleton, IH. lia. Qed.
imports: stdpp(finite) stdpp(options)