proposition: Lemma seq_add len1 len2 start : seq start (len1 + len2) = seq start len1 ++ seq (start + len1) len2.
proof: Proof. rewrite seq_split with (x := len1); try lia. f_equal; f_equal; lia. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation