@[simp]

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

theorem Array.sum_append_int {as₁ as₂ : Array Int} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum

theorem Array.sum_reverse_int (xs : Array Int) : xs.reverse.sum = xs.sum

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

theorem Array.min_mul_length_le_sum_int {xs : Array Int} (h : xs ≠ #[]) : xs.min h * ↑xs.size ≤ xs.sum

theorem Array.mul_length_le_sum_of_min?_eq_some_int {x : Int} {xs : Array Int} (h : xs.min? = some x) : x * ↑xs.size ≤ xs.sum

theorem Array.min_le_sum_div_length_int {xs : Array Int} (h : xs ≠ #[]) : xs.min h ≤ xs.sum / ↑xs.size

theorem Array.le_sum_div_length_of_min?_eq_some_int {x : Int} {xs : Array Int} (h : xs.min? = some x) : x ≤ xs.sum / ↑xs.size

theorem Array.sum_le_max_mul_length_int {xs : Array Int} (h : xs ≠ #[]) : xs.sum ≤ xs.max h * ↑xs.size

theorem Array.sum_le_max_mul_length_of_max?_eq_some_int {x : Int} {xs : Array Int} (h : xs.max? = some x) : xs.sum ≤ x * ↑xs.size

theorem Array.sum_div_length_le_max_int {xs : Array Int} (h : xs ≠ #[]) : xs.sum / ↑xs.size ≤ xs.max h

theorem Array.sum_div_length_le_max_of_max?_eq_some_int {x : Int} {xs : Array Int} (h : xs.max? = some x) : xs.sum / ↑xs.size ≤ x