rw [add_comm t, add_one_mul s, mul_add_one s, add_assoc]
case succ
t s : ℕ
ih : ascFactorial t s ≤ s ! * (t + 1) ^ s
⊢ t + s + 1 ≤ (s + 1) * (t + 1)
case succ
t s : ℕ
ih : ascFactorial t s ≤ s ! * (t + 1) ^ s
⊢ s + (t + 1) ≤ s * t + s + (t + 1)