Utils

Utility lemmas for Apportionmentlib.

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.