proposition: Lemma seq_split_perm : forall l a, a < l -> exists l', Permutation (seq 0 l) (a :: l') /\ ~ In a l'.
proof: Proof. ins; eapply In_NoDup_Permutation; eauto using nodup_seq; apply in_seq_iff; lia. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation