proposition: Lemma Permutation_cons_inv_r l k x : k ≡ₚ x :: l → ∃ k1 k2, k = k1 ++ x :: k2 ∧ l ≡ₚ k1 ++ k2.
proof: Proof. intros Hk. assert (∃ i, k !! i = Some x) as [i Hi]. { apply elem_of_list_lookup. rewrite Hk, elem_of_cons; auto. } exists (take i k), (drop (S i) k). split. - by rewrite take_drop_middle. - rewrite <-delete_take_drop. apply (inj (x ::.)). by rewrite <-Hk, <-(delete_Permutation k) by done. Qed.
imports: stdpp(options)