case zero

⊢ choose zero 2 = zero * (zero - 1) / 2

case succ
n : ℕ
ih : choose n 2 = n * (n - 1) / 2
⊢ choose (succ n) 2 = succ n * (succ n - 1) / 2
n : ℕ
⊢ choose n 2 = n * (n - 1) / 2
induction' n with n ih
case succ
n : ℕ
ih : choose n 2 = n * (n - 1) / 2
⊢ choose (succ n) 2 = succ n * (succ n - 1) / 2
case zero

⊢ choose zero 2 = zero * (zero - 1) / 2

case succ
n : ℕ
ih : choose n 2 = n * (n - 1) / 2
⊢ choose (succ n) 2 = succ n * (succ n - 1) / 2
. simp
no goals
case zero

⊢ choose zero 2 = zero * (zero - 1) / 2
simp
case succ
n : ℕ
ih : choose n 2 = n * (n - 1) / 2
⊢ choose n 1 + n * (n - 1) / 2 = n * (n - 1) / 2 + n
case succ
n : ℕ
ih : choose n 2 = n * (n - 1) / 2
⊢ choose (succ n) 2 = succ n * (succ n - 1) / 2
rw [triangle_succ n, choose, ih]
no goals
case succ
n : ℕ
ih : choose n 2 = n * (n - 1) / 2
⊢ choose n 1 + n * (n - 1) / 2 = n * (n - 1) / 2 + n
simp [add_comm]