Add a couple lemmas about product in Data.List.Properties

CHANGELOG.md

@@ -48,6 +48,12 @@ New modules
 Additions to existing modules
 -----------------------------
 
+* In `Data.List.Properties`:
+  ```agda
+  nonZero-product : All NonZero ns → NonZero (product ns)
+  ∈⇒≤product : n ∈ ns → All NonZero ns → n ≤ product ns
+  ```
+
 * In `Data.List.Relation.Unary.All`:
   ```agda
   search : Decidable P → ∀ xs → All (∁ P) xs ⊎ Any P xs

src/Data/List/Properties.agda

@@ -842,6 +842,27 @@ sum-++ (x ∷ xs) ys = begin
 ∈⇒∣product {n} {n ∷ ns} (here  refl) = divides (product ns) (*-comm n (product ns))
 ∈⇒∣product {n} {m ∷ ns} (there n∈ns) = ∣n⇒∣m*n m (∈⇒∣product n∈ns)
 
+nonZero-product : ∀ {ns} → All NonZero ns → NonZero (product ns)
+nonZero-product [] = _
+nonZero-product {n ∷ ns} (nzn ∷ nzns) = m*n≢0 n (product ns)
+  where instance
+    _ = nzn
+    _ = nonZero-product nzns
+
+∈⇒≤product : ∀ {n ns} → n ∈ ns → All NonZero ns → n ≤ product ns
+∈⇒≤product {n} {m ∷ ms} (here n≡m) (_ ∷ nzms) rewrite n≡m =
+  m≤m*n m (product ms)
+  where instance _ = nonZero-product nzms
+∈⇒≤product {n} {m ∷ ms} (there n∈ns) (nz ∷ nzns) = begin-ordered
+  n               ≤⟨ ∈⇒≤product n∈ns nzns ⟩
+  product ms      ≤⟨ m≤n*m (product ms) m ⟩
+  m * product ms  ∎-ordered
+  where
+  instance _ = nz
+  open ≤-Reasoning using (step-≤)
+    renaming ( begin_ to begin-ordered_ ; _∎ to _∎-ordered)
+
+
 ------------------------------------------------------------------------
 -- applyUpTo