proposition: Lemma seqS a n : seq a (S n) = seq a n ++ (a + n) :: nil.
proof: Proof. revert a; induction n; ins. f_equal; lia. rewrite IHn; do 3 f_equal; lia. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation