case zero

⊢ multichoose 1 zero = 1

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

⊢ multichoose 1 zero = 1
simp