refine' (div_lt_div_of_lt_left _ _ (factorial_bound_exp_of_ne_zero ht)).trans_eq _
n t : ℕ
hn : n ≠ 0
ht : t ≠ 0
⊢ ↑n ^ t / ↑t ! < (rexp 1 * ↑n / ↑t) ^ t
case refine'_1
n t : ℕ
hn : n ≠ 0
ht : t ≠ 0
⊢ 0 < ↑n ^ t

case refine'_2
n t : ℕ
hn : n ≠ 0
ht : t ≠ 0
⊢ 0 < (↑t / rexp 1) ^ t

case refine'_3
n t : ℕ
hn : n ≠ 0
ht : t ≠ 0
⊢ ↑n ^ t / (↑t / rexp 1) ^ t = (rexp 1 * ↑n / ↑t) ^ t