simp_rw [tsub_zero,hn,Nat.choose_zero_succ,Nat.zero_div,zero_mul,mul_zero,add_zero,zero_pow' ,zero_mul,mul_zero]
case inl
t n : ℕ
t1 : t + 1 - 1 = t
a : ℕ := n / (t + 1)
b : ℕ := n % (t + 1)
n2 : b < t + 1
n3 : t + 1 - 0 + 0 = t + 1
n1 : (t + 1) * a + 0 = 0
hb : b = 0
hn : n = 0
⊢ (t + 1 - 0) * a ^ 2 + 0 * (a + 1) ^ 2 +
      2 * (a ^ 2 * Nat.choose (t + 1 - 0) 2 + a * (a + 1) * 0 * (t + 1 - 0) + (a + 1) ^ 2 * Nat.choose 0 2) =
    0 ^ 2
no goals