theorem List.prod_eq_zero_iff_exists_zero_nat {l : List Nat} : l.prod = 0 ↔ ∃ (x : Nat), x ∈ l ∧ x = 0

theorem List.prod_pos_iff_forall_pos_nat {l : List Nat} : 0 < l.prod ↔ ∀ (x : Nat), x ∈ l → 0 < x

@[simp]

theorem List.prod_replicate_nat {n a : Nat} : (replicate n a).prod = a ^ n

theorem List.prod_append_nat {l₁ l₂ : List Nat} : (l₁ ++ l₂).prod = l₁.prod * l₂.prod

theorem List.prod_reverse_nat (xs : List Nat) : xs.reverse.prod = xs.prod

theorem List.prod_eq_foldl_nat {xs : List Nat} : xs.prod = foldl (fun (x1 x2 : Nat) => x1 * x2) 1 xs