case zero
a c : ℕ
⊢ choose a c ≤ choose (a + zero) c

case succ
a c b_n : ℕ
b_ih : choose a c ≤ choose (a + b_n) c
⊢ choose a c ≤ choose (a + succ b_n) c
a b c : ℕ
⊢ choose a c ≤ choose (a + b) c
induction' b with b_n b_ih
no goals
case succ
a c b_n : ℕ
b_ih : choose a c ≤ choose (a + b_n) c
⊢ choose a c ≤ choose (a + succ b_n) c
exact le_trans b_ih (choose_le_succ (a + b_n) c)
no goals
case zero
a c : ℕ
⊢ choose a c ≤ choose (a + zero) c
simp