proposition: Lemma submseteq_Permutation l1 l2 : l1 ⊆+ l2 → ∃ k, l2 ≡ₚ l1 ++ k.
proof: Proof. induction 1 as [|x y l ? [k Hk]| |x l1 l2 ? [k Hk]|l1 l2 l3 ? [k Hk] ? [k' Hk']]. - by eexists []. - exists k. by rewrite Hk. - eexists []. rewrite (right_id_L [] (++)). by constructor. - exists (x :: k). by rewrite Hk, Permutation_middle. - exists (k ++ k'). by rewrite Hk', Hk, (assoc_L (++)). Qed.
imports: stdpp(options)