proposition: Lemma length_eq_add A (l : list A) m n : length l = m + n <-> exists l' l'', l = l' ++ l'' /\ length l' = m /\ length l'' = n.
proof: Proof. split; ins; desf; eauto using length_app. revert m H; induction l; ins. destruct m; ins; desf; exists nil, nil; ins. destruct m; [eexists nil, _; ins|]. forward apply (IHl m) as X; ins; desf. eexists (_ :: _), _; ins. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation