rw [tN,tN']
t n : ℕ
⊢ turanNumb' t n + 2 * turanNumb t n = n ^ 2
t n : ℕ
⊢ (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