@[simp]

theorem Vector.sum_replicate_int {n : Nat} {a : Int} : (replicate n a).sum = ↑n * a

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

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

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