cases n with
| zero => rfl
| succ n =>
  rw [Nat.choose,Nat.choose_one_right,mul_add,ih]
  rw [succ_sub_succ_eq_sub,tsub_zero,mul_comm _ n,← add_mul];
  congr; rw [add_comm]
case succ
n : ℕ
ih : 2 * Nat.choose n 2 = n * (n - 1)
⊢ 2 * Nat.choose (succ n) 2 = succ n * (succ n - 1)
no goals