Theorem: Nat.choose_add_le_pow_left (ExponentialRamsey/Prereq/Mathlib/Data/Nat/Choose/Basic.lean)

State before:
s t : ℕ
⊢ choose (s + t) s ≤ (t + 1) ^ s
Tactic:
rw [add_comm, choose_eq_asc_factorial_div_factorial]
State after:
s t : ℕ
⊢ ascFactorial t s / s ! ≤ (t + 1) ^ s

State before:
s t : ℕ
⊢ ascFactorial t s / s ! ≤ (t + 1) ^ s
Tactic:
exact Nat.div_le_of_le_mul asc_le_pow_mul_factorial
State after:
no goals