unfold Bal at hb
t n : ℕ
P : ℕ → ℕ
hb : Bal t n P
f : ℕ → ℕ
⊢ ∑ i in range (t + 1), f (P i) = (t + 1 - n % (t + 1)) * f (n / (t + 1)) + n % (t + 1) * f (n / (t + 1) + 1)
t n : ℕ
P : ℕ → ℕ
hb : Balanced t P ∧ psum t P = n
f : ℕ → ℕ
⊢ ∑ i in range (t + 1), f (P i) = (t + 1 - n % (t + 1)) * f (n / (t + 1)) + n % (t + 1) * f (n / (t + 1) + 1)