proposition: Lemma prefix_app_r_inverse: forall ys1 xs ys2, prefix xs (ys1 ++ ys2) -> prefix xs ys1 \/ exists ys2a, xs = ys1 ++ ys2a /\ prefix ys2a ys2.
proof: Proof. Proof using. induction ys1 as [ | y ys1 ]; simpl; intros. { right. exists xs. rew_list in *. eauto. } { destruct xs as [ | x xs ]. { eauto using prefix_nil. } { rew_list in *. forwards: prefix_cons_cons_inverse. { eauto. } unpack. subst y. forwards [ ? | (ys2a&?&?) ]: IHys1. { eauto. } { eauto using prefix_cons_cons. } { right. eexists ys2a. rew_list. subst xs. eauto. } } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation LibList)