proposition: Lemma sublist_app_r l k1 k2 : l `sublist_of` k1 ++ k2 ↔ ∃ l1 l2, l = l1 ++ l2 ∧ l1 `sublist_of` k1 ∧ l2 `sublist_of` k2.
proof: Proof. split. - revert l k2. induction k1 as [|y k1 IH]; intros l k2; simpl. { eexists [], l. by repeat constructor. } rewrite sublist_cons_r. intros [?|(l' & ? &?)]; subst. + destruct (IH l k2) as (l1&l2&?&?&?); trivial; subst. exists l1, l2. auto using sublist_cons. + destruct (IH l' k2) as (l1&l2&?&?&?); trivial; subst. exists (y :: l1), l2. auto using sublist_skip. - intros (?&?&?&?&?); subst. auto using sublist_app. Qed.
imports: stdpp(options)