rw [Nat.choose,Nat.choose_one_right,mul_add,ih]
case succ.succ
n : ℕ
ih : 2 * Nat.choose (succ n) 2 = succ n * (succ n - 1)
⊢ 2 * Nat.choose (succ (succ n)) 2 = succ (succ n) * (succ (succ n) - 1)
case succ.succ
n : ℕ
ih : 2 * Nat.choose (succ n) 2 = succ n * (succ n - 1)
⊢ 2 * (n + 1) + succ n * (succ n - 1) = succ (succ n) * (succ (succ n) - 1)