proposition: Lemma list_app_eq_simpl (l l0 l' l0' : list A) : l ++ l' = l0 ++ l0' -> length l <= length l0 -> exists lr, l0 = l ++ lr /\ l' = lr ++ l0'.
proof: Proof. revert l0; induction l; ins; eauto. destruct l0; ins; desf; try lia. eapply IHl in H; desf; eauto; lia. Qed.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt