refine' (div_le_div_of_le_left _ _ factorial_bound_exp).trans _
case inr
n t : ℕ
h : t > 0
⊢ ↑n ^ t / ↑t ! ≤ (rexp 1 * ↑n / ↑t) ^ t
case inr.refine'_1
n t : ℕ
h : t > 0
⊢ 0 ≤ ↑n ^ t

case inr.refine'_2
n t : ℕ
h : t > 0
⊢ 0 < (↑t / rexp 1) ^ t

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