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

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

@[simp]

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

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

theorem Array.sum_reverse_nat (xs : Array Nat) : xs.reverse.sum = xs.sum

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

theorem Array.min_mul_length_le_sum_nat {xs : Array Nat} (h : xs ≠ #[]) : xs.min h * xs.size ≤ xs.sum

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

theorem Array.min_le_sum_div_length_nat {xs : Array Nat} (h : xs ≠ #[]) : xs.min h ≤ xs.sum / xs.size

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

theorem Array.sum_le_max_mul_length_nat {xs : Array Nat} (h : xs ≠ #[]) : xs.sum ≤ xs.max h * xs.size

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

theorem Array.sum_div_length_le_max_nat {xs : Array Nat} (h : xs ≠ #[]) : xs.sum / xs.size ≤ xs.max h

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