proposition: Lemma map_eq_app_inv A B (f : A -> B) l l1 l2 : map f l = l1 ++ l2 -> exists l1' l2', l = l1' ++ l2' /\ map f l1' = l1 /\ map f l2' = l2.
proof: Proof. apply map_eq_app. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation