proposition: Lemma seq_split : forall x a y, x <= y -> seq a y = seq a x ++ seq (x + a) (y - x).
proof: Proof. induction x; ins; rewrite ?Nat.sub_0_r; ins. destruct y; ins; try lia. f_equal; rewrite IHx; repeat (f_equal; try lia). Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation