@[simp]

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

theorem List.sum_append_int {l₁ l₂ : List Int} : (l₁ ++ l₂).sum = l₁.sum + l₂.sum

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

theorem List.min_mul_length_le_sum_int {xs : List Int} (h : xs ≠ []) : xs.min h * ↑xs.length ≤ xs.sum

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

theorem List.min_le_sum_div_length_int {xs : List Int} (h : xs ≠ []) : xs.min h ≤ xs.sum / ↑xs.length

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

theorem List.sum_le_max_mul_length_int {xs : List Int} (h : xs ≠ []) : xs.sum ≤ xs.max h * ↑xs.length

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

theorem List.sum_div_length_le_max_int {xs : List Int} (h : xs ≠ []) : xs.sum / ↑xs.length ≤ xs.max h

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