diff --git a/stdpp/list.v b/stdpp/list.v
index 68f54f809b30fe89e0cf39fa5bb52669e945d08d..81f61fd16a5a8fc80bdcb0fd25ab61d5ab4e8f16 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -2033,6 +2033,13 @@ Section filter.
     rewrite reverse_cons, filter_app, IHl, !filter_cons.
     case_decide; [by rewrite reverse_cons|by rewrite filter_nil, app_nil_r].
   Qed.
+
+  Lemma filter_app_complement l : filter P l ++ filter (λ x, ¬P x) l ≡ₚ l.
+  Proof.
+    induction l as [|x l IH]; simpl; [done|]. case_decide.
+    - rewrite decide_False by naive_solver. simpl. by rewrite IH.
+    - rewrite decide_True by done. by rewrite <-Permutation_middle, IH.
+  Qed.
 End filter.
 
 Lemma list_filter_iff (P1 P2 : A → Prop)