case zero

⊢ multichoose zero 1 = zero

case succ
n : ℕ
IH : multichoose n 1 = n
⊢ multichoose (succ n) 1 = succ n
n : ℕ
⊢ multichoose n 1 = n
induction' n with n IH
no goals
case succ
n : ℕ
IH : multichoose n 1 = n
⊢ multichoose (succ n) 1 = succ n
simp [multichoose_succ_succ n 0, IH]
no goals
case zero

⊢ multichoose zero 1 = zero
simp