proposition: Fact prefix_app_inv l1 l2 r1 r2 : l1++l2 <p r1++r2 -> { l1 <p r1 } + { r1 <p l1 }.
proof: Proof. revert l2 r1 r2; induction l1 as [ | x l1 IH ]. left; apply in_prefix_0. intros l2 [ | y r1 ] r2. right; apply in_prefix_0. simpl; intros H; apply prefix_inv in H. destruct H as (E & H); subst y. destruct IH with (1 := H); [ left | right ]; apply in_prefix_1; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)