n k : ℕ
⊢ (n + 1) * (n + 1) ^ (k + 1) < (n + (k + 1) + 1) * ascFactorial n (k + 1)
n k : ℕ
⊢ (n + 1) ^ (k + 2) < ascFactorial n (k + 2)
rw [pow_succ, ascFactorial, mul_comm]
no goals
n k : ℕ
⊢ (n + 1) * (n + 1) ^ (k + 1) < (n + (k + 1) + 1) * ascFactorial n (k + 1)
exact
  Nat.mul_lt_mul (Nat.add_lt_add_right (Nat.lt_add_of_pos_right succ_pos') 1)
    (pow_succ_le_ascFactorial n _) (pow_pos succ_pos' _)