n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
⊢ choose (n + 1) (k + 1) = 0
n k : ℕ
hk : n + 1 < k + 1
⊢ choose (n + 1) (k + 1) = 0
have hnk : n < k := lt_of_succ_lt_succ hk
n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
hnk1 : n < k + 1
⊢ choose (n + 1) (k + 1) = 0
n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
⊢ choose (n + 1) (k + 1) = 0
have hnk1 : n < k + 1 := lt_of_succ_lt hk
no goals
n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
hnk1 : n < k + 1
⊢ choose (n + 1) (k + 1) = 0
rw [choose_succ_succ, choose_eq_zero_of_lt hnk, choose_eq_zero_of_lt hnk1]