proposition: Lemma seq_split_gen : forall l n a, n <= a < n + l -> seq n l = seq n (a - n) ++ a :: seq (S a) (l + n - a - 1).
proof: Proof. induction l; ins; desf; ins; try lia. repeat f_equal; lia. destruct (eqP n (S n0)); subst. replace (n0 - n0) with 0 by lia; ins; repeat f_equal; lia. rewrite IHl with (a := S n0); try lia. desf; ins; try replace (n0 - n2) with (S (n0 - S n2)) by lia; ins; repeat (f_equal; try lia). Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation