theorem Vector.sum_pos_iff_exists_pos_nat {n : Nat} {xs : Vector Nat n} : 0 < xs.sum ↔ ∃ (x : Nat), x ∈ xs ∧ 0 < x

theorem Vector.sum_eq_zero_iff_forall_eq_nat {n : Nat} {xs : Vector Nat n} : xs.sum = 0 ↔ ∀ (x : Nat), x ∈ xs → x = 0

@[simp]

theorem Vector.sum_replicate_nat {n a : Nat} : (replicate n a).sum = n * a

theorem Vector.sum_append_nat {n : Nat} {as₁ as₂ : Vector Nat n} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum

theorem Vector.sum_reverse_nat {n : Nat} (xs : Vector Nat n) : xs.reverse.sum = xs.sum

theorem Vector.sum_eq_foldl_nat {n : Nat} {xs : Vector Nat n} : xs.sum = foldl (fun (x1 x2 : Nat) => x1 + x2) 0 xs