case zero

⊢ multichoose 2 zero = zero + 1

case succ
k : ℕ
IH : multichoose 2 k = k + 1
⊢ multichoose 2 (succ k) = succ k + 1
k : ℕ
⊢ multichoose 2 k = k + 1
induction' k with k IH
case succ
k : ℕ
IH : multichoose 2 k = k + 1
⊢ multichoose 1 (k + 1) + (k + 1) = succ k + 1
case succ
k : ℕ
IH : multichoose 2 k = k + 1
⊢ multichoose 2 (succ k) = succ k + 1
rw [multichoose, IH]
no goals
case succ
k : ℕ
IH : multichoose 2 k = k + 1
⊢ multichoose 1 (k + 1) + (k + 1) = succ k + 1
simp [add_comm, succ_eq_add_one]
no goals
case zero

⊢ multichoose 2 zero = zero + 1
simp