congr
case succ.succ
n : ℕ
ih : 2 * Nat.choose (succ n) 2 = succ n * (succ n - 1)
⊢ (2 + n) * (n + 1) = succ (succ n) * (succ (succ n) - 1)
case succ.succ.e_a
n : ℕ
ih : 2 * Nat.choose (succ n) 2 = succ n * (succ n - 1)
⊢ 2 + n = succ (succ n)