have n3 : t + 1 - n % (t + 1) + n % (t + 1) = t + 1 := tsub_add_cancel_of_le (le_of_lt n2)
t n : ℕ
t1 : t + 1 - 1 = t
n1 : (t + 1) * (n / (t + 1)) + n % (t + 1) = n
n2 : n % (t + 1) < t + 1
⊢ (t + 1 - n % (t + 1)) * (n / (t + 1)) ^ 2 + n % (t + 1) * (n / (t + 1) + 1) ^ 2 +
      2 *
        ((n / (t + 1)) ^ 2 * Nat.choose (t + 1 - n % (t + 1)) 2 +
            n / (t + 1) * (n / (t + 1) + 1) * (n % (t + 1)) * (t + 1 - n % (t + 1)) +
          (n / (t + 1) + 1) ^ 2 * Nat.choose (n % (t + 1)) 2) =
    n ^ 2
t n : ℕ
t1 : t + 1 - 1 = t
n1 : (t + 1) * (n / (t + 1)) + n % (t + 1) = n
n2 : n % (t + 1) < t + 1
n3 : t + 1 - n % (t + 1) + n % (t + 1) = t + 1
⊢ (t + 1 - n % (t + 1)) * (n / (t + 1)) ^ 2 + n % (t + 1) * (n / (t + 1) + 1) ^ 2 +
      2 *
        ((n / (t + 1)) ^ 2 * Nat.choose (t + 1 - n % (t + 1)) 2 +
            n / (t + 1) * (n / (t + 1) + 1) * (n % (t + 1)) * (t + 1 - n % (t + 1)) +
          (n / (t + 1) + 1) ^ 2 * Nat.choose (n % (t + 1)) 2) =
    n ^ 2