diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3867278c6c..d3b995f11b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -130,6 +130,11 @@ Additions to existing modules
   gcd[n,n]≡n : ∀ n → gcd n n ≡ n
   ```
 
+* In `Data.Nat.ListAction.Properties`:
+  ```agda
+  product-locate : ∀ ns → product ns ≡ 0 → 0 ∈ ns
+  ```
+
 * In `Data.Rational.Properties`:
   ```agda
   ↥[i/1]≡i  : (i : ℤ) → ↥ (i / 1) ≡ i
diff --git a/src/Data/Nat/ListAction/Properties.agda b/src/Data/Nat/ListAction/Properties.agda
index 90c644c7fb..34756b6ab1 100644
--- a/src/Data/Nat/ListAction/Properties.agda
+++ b/src/Data/Nat/ListAction/Properties.agda
@@ -27,7 +27,9 @@ open import Data.Nat.Properties
   using (+-assoc; *-assoc; *-identityˡ; m*n≢0; m≤m*n; m≤n⇒m≤o*n
         ; +-0-commutativeMonoid; *-1-commutativeMonoid
         ; *-zeroˡ; *-zeroʳ; *-distribˡ-+; *-distribʳ-+
-        ; ^-zeroˡ; ^-distribʳ-*)
+        ; ^-zeroˡ; ^-distribʳ-*; m*n≡0⇒m≡0∨n≡0)
+open import Data.Sum.Base using ([_,_]′)
+open import Function.Base using (_∘′_)
 open import Relation.Binary.Core using (_Preserves_⟶_)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; refl; sym; trans; cong)
@@ -80,6 +82,11 @@ product-++ (m ∷ ms) ns = begin
 ∈⇒∣product {ns = n ∷ ns} (here  refl) = m∣m*n (product ns)
 ∈⇒∣product {ns = m ∷ ns} (there n∈ns) = ∣n⇒∣m*n m (∈⇒∣product n∈ns)
 
+product-locate : ∀ ns → product ns ≡ 0 → 0 ∈ ns
+product-locate (n ∷ ns) =
+  [ here ∘′ sym , there ∘′ product-locate ns ]′ ∘′ m*n≡0⇒m≡0∨n≡0 n
+
+
 product≢0 : All NonZero ns → NonZero (product ns)
 product≢0 []           = _
 product≢0 (n≢0 ∷ ns≢0) = m*n≢0 _ _ {{n≢0}} {{product≢0 ns≢0}}