induction' s with s ih
s t : ℕ
⊢ ascFactorial t s ≤ s ! * (t + 1) ^ s
case zero
t : ℕ
⊢ ascFactorial t zero ≤ zero ! * (t + 1) ^ zero

case succ
t s : ℕ
ih : ascFactorial t s ≤ s ! * (t + 1) ^ s
⊢ ascFactorial t (succ s) ≤ (succ s)! * (t + 1) ^ succ s