no goals
n : ℕ
⊢ ascFactorial n 0 ≤ (n + 0) ^ 0
rw [ascFactorial_zero, pow_zero]
n k : ℕ
⊢ succ (n + k) * ascFactorial n k ≤ succ (n + k) * succ (n + k) ^ k
n k : ℕ
⊢ ascFactorial n (k + 1) ≤ (n + (k + 1)) ^ (k + 1)
rw [ascFactorial_succ, pow_succ, ← add_assoc,
← Nat.succ_eq_add_one (n + k), mul_comm _ (succ (n + k))]
no goals
n k : ℕ
⊢ succ (n + k) * ascFactorial n k ≤ succ (n + k) * succ (n + k) ^ k
exact
  Nat.mul_le_mul_of_nonneg_left
    ((ascFactorial_le_pow_add _ k).trans (Nat.pow_le_pow_of_le_left (le_succ _) _))