proposition: Lemma In_split2 : forall A (x: A) l (IN: In x l), exists l1 l2, l = l1 ++ x :: l2 /\ ~ In x l1.
proof: Proof. induction l; ins; desf; [by eexists nil; ins; eauto|]. destruct (classic (a = x)); desf; [by eexists nil; ins; eauto|]. apply IHl in IN; desf; eexists (_ :: _); repeat eexists; ins; intro; desf. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation