rw [div_pow, ← rpow_nat_cast (exp 1), exp_one_rpow, div_lt_iff, ← div_lt_iff']
n : ℕ
hn : n ≠ 0
⊢ (↑n / rexp 1) ^ n < ↑n !
n : ℕ
hn : n ≠ 0
⊢ ↑n ^ n / ↑n ! < rexp ↑n

n : ℕ
hn : n ≠ 0
⊢ 0 < ↑n !

n : ℕ
hn : n ≠ 0
⊢ 0 < rexp ↑n