rw [bal_sum' hb1, ← div_add_mod n (t + 1)] at hb2
case intro
t n : ℕ
P : ℕ → ℕ
hb1 : Balanced t P
hb2 : psum t P = n
⊢ minP t P = n / (t + 1) ∧ card (largeParts (_ : Balanced t P)) = n % (t + 1)
case intro
t n : ℕ
P : ℕ → ℕ
hb1 : Balanced t P
hb2✝ : psum t P = n
hb2 : (t + 1) * minP t P + card (largeParts hb1) = (t + 1) * (n / (t + 1)) + n % (t + 1)
⊢ minP t P = n / (t + 1) ∧ card (largeParts (_ : Balanced t P)) = n % (t + 1)