rw [ascFactorial_succ, factorial_succ, pow_succ', mul_mul_mul_comm]
case succ
t s : ℕ
ih : ascFactorial t s ≤ s ! * (t + 1) ^ s
⊢ ascFactorial t (succ s) ≤ (succ s)! * (t + 1) ^ succ s
case succ
t s : ℕ
ih : ascFactorial t s ≤ s ! * (t + 1) ^ s
⊢ (t + s + 1) * ascFactorial t s ≤ (s + 1) * (t + 1) * (s ! * (t + 1) ^ s)