proposition: Lemma seq_split0 : forall l a, a < l -> seq 0 l = seq 0 a ++ a :: seq (S a) (l - a - 1).
proof: Proof. ins; rewrite seq_split_gen with (a := a); repeat f_equal; lia. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation