proposition: Lemma set_seq_subseteq_len_gt start1 len1 start2 len2 : set_seq (C:=C) start1 len1 ⊆ set_seq (C:=C) start2 len2 → len1 ≤ len2.
proof: Proof. destruct len1 as [|len1]. - set_unfold. lia. - rewrite set_seq_subseteq; lia. Qed.
imports: stdpp(finite) stdpp(options)