diff --git a/theories/list.v b/theories/list.v
index b1cc30e7cfafc031e8f2aa36b469c34a3dde9298..f6a831353482ccc65b3dd9b9c096d0c21cf326b6 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1771,6 +1771,27 @@ Proof.
     by rewrite <-Hk, <-(delete_Permutation k) by done.
 Qed.
 
+Lemma Permutation_cross_split l la lb lc ld :
+  la ++ lb ≡ₚ l →
+  lc ++ ld ≡ₚ l →
+  ∃ lac lad lbc lbd,
+    lac ++ lad ≡ₚ la ∧ lbc ++ lbd ≡ₚ lb ∧ lac ++ lbc ≡ₚ lc ∧ lad ++ lbd ≡ₚ ld.
+Proof.
+  intros <-. revert lc ld.
+  induction la as [|x la IH]; simpl; intros lc ld Hperm.
+  { exists [], [], lc, ld. by rewrite !(right_id_L [] (++)). }
+  assert (x ∈ lc ++ ld)
+    as [[lc' Hlc]%elem_of_Permutation|[ld' Hld]%elem_of_Permutation]%elem_of_app.
+  { rewrite Hperm, elem_of_cons. auto. }
+  - rewrite Hlc in Hperm. simpl in Hperm. apply (inj (x ::.)) in Hperm.
+    apply IH in Hperm as (lac&lad&lbc&lbd&Ha&Hb&Hc&Hd).
+    exists (x :: lac), lad, lbc, lbd; simpl. by rewrite Ha, Hb, Hc, Hd.
+  - rewrite Hld, <-Permutation_middle in Hperm. apply (inj (x ::.)) in Hperm.
+    apply IH in Hperm as (lac&lad&lbc&lbd&Ha&Hb&Hc&Hd).
+    exists lac, (x :: lad), lbc, lbd; simpl.
+    by rewrite <-Permutation_middle, Ha, Hb, Hc, Hd.
+Qed.
+
 Lemma Permutation_inj l1 l2 :
   Permutation l1 l2 ↔
     length l1 = length l2 ∧