cases' Nat.eq_zero_or_pos t with h h
n t : ℕ
⊢ ↑(Nat.choose n t) ≤ (rexp 1 * ↑n / ↑t) ^ t
case inl
n t : ℕ
h : t = 0
⊢ ↑(Nat.choose n t) ≤ (rexp 1 * ↑n / ↑t) ^ t

case inr
n t : ℕ
h : t > 0
⊢ ↑(Nat.choose n t) ≤ (rexp 1 * ↑n / ↑t) ^ t