Utils

Utility lemmas for the Apportionment library: a positivity criterion for the sum of a vector of natural numbers, and a closed form for the sum of a length-four vector.

theorem sum_pos_iff_exists_pos {n : ℕ} {v : Vector ℕ n} : 0 < v.sum ↔ ∃ (i : Fin n), 0 < v[i]

A vector of natural numbers has positive sum iff at least one component is positive.

theorem Vector.sum_four (v : Vector ℕ 4) : v.sum = v[0] + v[1] + v[2] + v[3]

The sum of a length-4 vector equals the sum of its components.