refine' Nat.mul_le_mul _ ih
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)
case succ
t s : ℕ
ih : ascFactorial t s ≤ s ! * (t + 1) ^ s
⊢ t + s + 1 ≤ (s + 1) * (t + 1)