diff --git a/CHANGELOG.md b/CHANGELOG.md
index f3e17fa961..a58227662c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -186,6 +186,10 @@ Additions to existing modules
   ∈⇒≤product   : All NonZero ns → n ∈ ns → n ≤ product ns
   concatMap-++ : concatMap f (xs ++ ys) ≡ concatMap f xs ++ concatMap f ys
   filter-≐     : P ≐ Q → filter P? ≗ filter Q?
+
+  partition-is-foldr : partition P? ≗ foldr (λ x → if does (P? x) then Product.map₁ (x ∷_)
+                                                                  else Product.map₂ (x ∷_))
+                                            ([] , [])
   ```
 
 * In `Data.List.Relation.Unary.Any.Properties`:
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index ab5aff8904..274b684a8d 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -1294,6 +1294,14 @@ module _ {P : Pred A p} (P? : Decidable P) where
   ...  | true  = Product.map s≤s m≤n⇒m≤1+n ih
   ...  | false = Product.map m≤n⇒m≤1+n s≤s ih
 
+  partition-is-foldr : partition P? ≗ foldr
+    (λ x → if does (P? x) then Product.map₁ (x ∷_) else Product.map₂ (x ∷_))
+    ([] , [])
+  partition-is-foldr [] = refl
+  partition-is-foldr (x ∷ xs) with ih ← partition-is-foldr xs | does (P? x)
+  ... | true =  cong (Product.map₁ (x ∷_)) ih
+  ... | false = cong (Product.map₂ (x ∷_)) ih
+
 ------------------------------------------------------------------------
 -- _ʳ++_