no goals
x✝ : ℕ
⊢ multichoose x✝ 0 = choose (x✝ + 0 - 1) 0
simp
no goals
k : ℕ
⊢ multichoose 0 (k + 1) = choose (0 + (k + 1) - 1) (k + 1)
simp
n k : ℕ
this : n + (k + 1) < n + 1 + (k + 1)
⊢ multichoose (n + 1) (k + 1) = choose (n + 1 + (k + 1) - 1) (k + 1)
n k : ℕ
⊢ multichoose (n + 1) (k + 1) = choose (n + 1 + (k + 1) - 1) (k + 1)
have : n + (k + 1) < (n + 1) + (k + 1) := add_lt_add_right (Nat.lt_succ_self _) _
n k : ℕ
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ multichoose (n + 1) (k + 1) = choose (n + 1 + (k + 1) - 1) (k + 1)
n k : ℕ
this : n + (k + 1) < n + 1 + (k + 1)
⊢ multichoose (n + 1) (k + 1) = choose (n + 1 + (k + 1) - 1) (k + 1)
have : (n + 1) + k < (n + 1) + (k + 1) := add_lt_add_left (Nat.lt_succ_self _) _
n k : ℕ
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ multichoose (n + 1) k + multichoose n (k + 1) = choose (n + k) k + choose (n + k) (succ k)
n k : ℕ
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ multichoose (n + 1) (k + 1) = choose (n + 1 + (k + 1) - 1) (k + 1)
erw [multichoose_succ_succ, add_comm, Nat.succ_add_sub_one, ← add_assoc, Nat.choose_succ_succ]
no goals
n k : ℕ
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ multichoose (n + 1) k + multichoose n (k + 1) = choose (n + k) k + choose (n + k) (succ k)
simp [multichoose_eq n (k+1), multichoose_eq (n+1) k]