proposition: Lemma set_seq_subseteq start1 len1 start2 len2 : 0 < len1 → set_seq (C:=C) start1 len1 ⊆ set_seq (C:=C) start2 len2 ↔ start2 ≤ start1 ∧ start1 + len1 ≤ start2 + len2.
proof: Proof. intros Hlen. set_unfold. split. - intros Hx. pose proof (Hx start1). pose proof (Hx (start1 + len1 - 1)). lia. - intros Heq x. lia. Qed.
imports: stdpp(finite) stdpp(options)