unfold Balanced at h
t : ℕ
P : ℕ → ℕ
h : Balanced t P
⊢ ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
⊢ ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1